Coq takes the ACM Software System Award
The ACM (Association for Computing Machinery) recently announced the selection of the Coq development team for the "Software System Award". This prize rewards a long-term group effort, which Inria has been supporting for some 30 years.
Another prize for the Coq software system—this time from the Association for Computing Machinery. After winning the SIGPLAN Programming Languages Software Award in January, Coq was singled out for the ACM's highest distinction for software, the Software System Award. With this award, Coq joins the hallowed ranks of Unix, TeX, TCP/IP, NCSA Mosaic, Java, Make, Apache and even the World Wide Web.
Inria can take pride in this collective accomplishment, which honours the whole development team behind Coq—particularly the nine recipients of the Software System Award :
- Thierry Coquand, University of Gothenburg;
- Gérard Huet, INRIA Paris - Rocquencourt;
- Christine Paulin-Mohring, University Paris Sud/INRIA Saclay-Ile de France;
- Bruno Barras, INRIA Saclay/École Polytechnique;
- Jean-Christophe Filliâtre, CNRS/INRIA Saclay-Ile-de-France;
- Hugo Herbelin, INRIA Paris - Rocquencourt;
- Chet Murthy, Google Inc.;
- Yves Bertot, INRIA Sophia Antipolis Méditerranée;
- Pierre Castéran, University of Bordeaux.
Based on theoretical foundations that were established 30 years ago, Coq has evolved to become a prized proof assistant for computer scientists, who use it as an aid for writing and checking programs. The highly effective tool is now winning over mathematicians too.
The award will be presented on June 21 in San Francisco.