Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows:

• the definition of interactively evaluated functions or predicates,
• to state mathematical theorems and software specifications,
• to develop interactively formal proofs of these theorems,
• to check these proofs by a small certification "kernel".

Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories.

Coq also includes

• a mecanism for automatic generation of certified programs from proofs of their specifications
• a graphical user interface based on gtk (CoqIde)
• a documentation tool (coqdoc)
• dependecy and makefile generation tools for Coq (coq_makefile and coqdep)
• a preprocessor for TeX files that include Coq commands (coq-tex)

Coq is written in the Objective Caml language and uses the Camlp4 Pre-processor-pretty-printer for Objective Caml. Coq is distributed under the GNU Lesser General Public Licence Version 2.1 (LGPL). It is currently available for Unix (including Mac OS X)

download install purchase purchase