Coq
|
|
In automated theorem proving, Coq is a proof assistant which handles mathematical assertions, checks mechanically proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions.
It was developed in France, in the LogiCal (http://logical.inria.fr/) project, jointly operated by INRIA, École Polytechnique, University Paris XI and CNRS (there was also formerly a group at École Normale Supérieure de Lyon). The team leaders are Pr Gilles Dowek and Pr Christine Paulin-Mohring. Coq is written in the Ocaml programming language.
Coq means "rooster" in French - and Thierry Coquand (along with Gérard Huet) developed the aforementioned calculus of constructions.
Benjamin Werner (of INRIA) and Georges Gonthier (of Microsoft Research, in Cambridge, England) used Coq to create a surveyable proof of the four color theorem, which was completed in September 2004.
See also
External links
- The Coq proof assistant (http://coq.inria.fr/)
- Development of theories and tactics: Four Color Theorem (http://www.inria.fr/rapportsactivite/RA2004/logical2004/uid40.html)es:Coq