Coq selected as recipient of the prestigious ACM Software System Award
from left to right : Vinton Cerf, Brent Hailpern, Yves Bertot, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, John White (ACM Chief Executive Officer). - @ACM
Yves Bertot, leader of Inria's Marelle project team, was invited to San Francisco on 21 June 2013, along with Bruno Barras, Pierre Castéran, Thierry Coquand, Jean-Christophe Filliâtre, Hugo Herbelin, Gérard P. Huet, Chetan Murthy and Christine Paulin-Mohring, to receive the prestigious Software System Award 2013, one of the highest distinctions awarded by AMC, the Association for Computing Machinery. The award, given on the same day as the Turing Award, was for the development of Coq, a proof management system, originally known as COC, the acronym for Calculus of Inductive Constructions. It was the first time in 40 years that the award had gone to a French team, what's more, to a team that also received the ACM SIGPLAN Programming Languages Software Award at the POPL 2014 conference.
"Coq is a proof assistant, in other words, it provides a language and environment for writing mathematical definitions and proofs," explains Christine Paulin-Mohring of University Paris-Sud and member of the TOCCATA research team, a joint project team involving University Paris Sud's Computer Science Research Laboratory (LRI) and Inria. Christine Paulin is one of the three founding members of the Coq system, together with her Inria colleagues Gérard Huet and Thierry Coquand. Coq's main function is to "check proof corrections; it's an impartial, uncompromising 'proof-reader' that doesn't let through a single development error or omission."
Jean-Christophe Filliâtre joined the team in 1994 for his DEA post-graduate degree and defended his PhD thesis in 1999. He worked on Coq's code to rework the architecture, more specifically to isolate the critical part of the system for greater security, which is an important issue given that Coq is used to certify other software. The researcher points out that what makes this tool so effective is that:"the user interacts with Coq to introduce definitions, state theorems and construct proofs, then the system verifies that these various items are valid."
In April 2004, Yves Bertot from Inria and Pierre Castéran from the University of Bordeaux co-wrote the first user's manual on the Coq system entitled: "Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions". The book provides a gradual introduction to the most novel features of the Coq system and describes them with the help of many examples and exercises. The book also addresses the problems most commonly encountered by advanced users of the system and offers solutions. It is regarded as one of the best works on programming language and is widely used by staudents and teachers alike.
The fruit of more than 30 years of development and contributions from many sources, the Coq program has been successfully used in various contexts:
- top-level certification of the security objectives of a chip card platform,
- the Four Colour Theorem, for which the completely mechanised demonstration was completed in 2004 by Georges Gonthier and Benjamin Werner,
- the Feit-Thompson Theorem, for which the proof was completed by Georges Gonthier and his team in September 2012,
- the CompCert C compiler optimising the C language, which is entirely programmed and proved by the Coq system.
Until recently it was used to detect a flaw in OpenSSL
"Coq is a fine example of the French research approach, thanks to which this collaborative project has been able to develop over the long term," the team declares with great satisfaction.