About:
The Coq tool is a proof assistant which is able to handle calculus assertions, to check proofs of these assertions mechanically, and to extract a certified program from the constructive proof of its formal specification.

Author:
The Coq Development Team <coq (at) inria (dot) fr> [contact developer]

Rating:	reset 1 2 3 4 5 6 7 8 9 10
(not rated)

Homepage:
http://coq.inria.fr/
Tar/GZ:
ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/coq-8.0pl3.tar.gz
Changelog:
ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/doc/Changes.html
RPM package:
ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/coq-8.0pl3-1.i386.rpm
OS X package:
ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/coq-8.0pl3-macosx.dmg
CVS tree (cvsweb):
http://coqcvs.inria.fr/cgi-bin/cvsweb/V7/?cvsroot=coq
Mailing list archive:
http://pauillac.inria.fr/pipermail/coq-club/2003/thread.html#end

Trove categories: [change]

[Development Status]		6 - Mature
[License]		OSI Approved :: GNU Lesser General Public License (LGPL)
[Operating System]		MacOS X, Microsoft :: Windows, POSIX, POSIX :: Linux
[Programming Language]		OCaml
[Topic]		Scientific/Engineering :: Mathematics

Dependencies: [change]
No dependencies filed

 Branches

Branch	Version	Last release	License	URLs
Default	8.0pl3	25-Aug-2006	GNU Lesser General Public License (LGPL)