Coq 8.2pl1

A formal proof management system

  Add it to your Download Basket!

 Add it to your Watch List!

0/5

Rate it!
send us
an update
LICENSE TYPE:
LGPL (GNU Lesser General Public License) 
USER RATING:
UNRATED
  0.0/5
DEVELOPED BY:
The Coq Team
HOMEPAGE:
coq.inria.fr
CATEGORY:
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!

SUBMIT