Coq

8.0 • 01 May 2004

Formal proof management system for mathematics.

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)

Requirements

Mac OS X 10.1 or later

Ratings

Overall

(2)

Current Version (8.x)

(2)

Details

Downloads: 2,810
Version Downloads: 1,929
Type: Education / Mathematics
License: Free
Date: 01 May 2004
Platform: OS X / PPC 32
Price: Free