Coq 8.2pl1

A formal proof management system

  Add it to your Download Basket!

 Add it to your Watch List!


Rate it!
send us
an update
LGPL (GNU Lesser General Public License) 
The Coq Team
ROOT \ Science and Engineering \ Mathematics
Coq is a software that provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Coq implements a program specification and mathematical higher-level language called Gallina that is based on an expressive formal language called the Calculus of Inductive Constructions that itself combines both a higher-order logic and a richly-typed functional programming language. Through a vernacular language of commands, Coq allows:

* to define functions or predicates, that can be evaluated efficiently;
* to state mathematical theorems and software specifications;
* to interactively develop formal proofs of these theorems;
* to machine-check these proofs by a relatively small certification "kernel";
* to extract certified programs to languages like Objective Caml, Haskell or Scheme.

As a proof development system, Coq provides interactive proof methods, decision and semi-decision algorithms, and a tactic language for letting the user define its own proof methods. Connection with external computer algebra system or theorem provers is available.

As a platform for the formalization of mathematics or the development of programs, Coq provides support for high-level notations, implicit contents and various other useful kinds of macros.

Coq comes with libraries for efficient arithmetics in N, Z and Q, libraries about lists, finite sets and finite maps, libraries on abstract sets, relations, classical analysis, etc.

Coq is released with:

* a graphical user interface based on gtk (CoqIde) (see screenshots),
* documentation tools (coqdoc and coq-tex) and a statistics tool (coqwc),
* dependency and makefile generation tools for Coq (coq_makefile and coqdep),
* a stand-alone proof verifier (coqchk, from Coq 8.2).

Last updated on August 11th, 2009

#proof management #calculus assertions #proof assistant #proof #management #calculus #assertions

Add your review!