Coq

Formal proof management system

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

Coq screenshot

License: GNU LGPL.

Tags: logic, automated theorem proving.

Interfaces: command line, X.

Source language: OCaml.

Staff

Maintainer: Benjamin Monate.

Developer: Benjamin Monate.

Contributors: Jean-Cristophe Filliâtre, Pierre Letouzey, Claude Marché.

Links

Homepage: http://coq.inria.fr/.

Documentation: http://coq.inria.fr/doc-eng.html.

Source repository: http://coq.inria.fr/distrib-eng.html.

Bug database: http://logical.futurs.inria.fr/cgi-bin/bugzilla/index.cgi.

Mailing lists

Support: coq-club@pauillac.inria.fr.