Coq

8.0 01 May 2004

Formal proof management system for mathematics.

2

Developer website: The LogiCal project

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