Coq

Coq is a program for machine-assisted proofs of mathematical statements.

Survey

In Coq formulating data type definitions and executable program elements and mathematical statements and proofs. The statements usually relate to the defined functions. Coq checks the formal correctness of proofs using his otherwise used type of auditor.

Furthermore, Coq supports the search for evidence and allows for example to extract from a formal program specification, including implementation and correctness proof of a ML program. This non- translatable type information is ignored. From ( necessarily constructive ) proofs of existence statements also target code can be generated.

Coq uses the calculus of inductive construction, a form of construction calculus. Coq is not a fully automated proof system, but knows some proof tactics and decision procedures.

Development

Coq is in France in the project TYPICAL (formerly Logical ) developed a joint project of INRIA, École Polytechnique, University of Paris-Sud and CNRS. Another working group consisted of the Ecole Normale Supérieure de Lyon. Team leader is Benjamin Werner.

Coq is developed in the Objective CAML, a ( mostly) functional programming language.

Name

The French word means Coq rooster or cockerel and is in the French tradition to appoint scientific development tools by animals. In addition, it is reminiscent of Thierry Coquand, who developed the design calculus together with Gérard Huet.

Four -color set

Georges Gonthier ( Microsoft Research, Cambridge, England) and Benjamin Werner ( INRIA ) generated with the help of Coq a manageable proof of the four - color theorem, which was completed in 2005.

As a side result of this work an extension of Coq called ssreflect ("small scale reflection" ) was born. Despite the name, most of the features of the extension can be used generally, not just for reflexive evidence. The current version ssreflect 1.2 is free, open - source software (license CeCILL ) and is compatible with Coq 8.2.