Coq

In automated theorem proving, Coq is a proof assistant which handles mathematics assertions, mechanically checks 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 .

Coq means rooster in French language - 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 =

*Intuitionistic Type Theory

=External links=

*[http://coq.inria.fr/ The Coq proof assistant] *[http://www.inria.fr/rapportsactivite/RA2004/logical2004/uid40.html Development of theories and tactics: Four Color Theorem] *[http://cocorico.cs.ru.nl/coqwiki A Wiki for Coq]