|
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.
Release focus: Minor feature enhancements
Changes:
The search depth argument of auto can be
parameterised in the Ltac language. The
constr_may_eval entry was added for tactic
extensions. A couple of lemmas of ZArith were
renamed. This concerns names containing O (the
letter), which is replaced by 0 (the number).
Author:
The Coq Development Team <coq __at__ inria __dot__ fr>
[contact developer]
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]
Dependencies:
[change]
No dependencies filed
|
|
» Rating:
(not rated)
» Vitality: 0.00% (Rank 11001)
» Popularity: 0.33% (Rank 16906)
 
(click to enlarge graphs)
Record hits: 4,064
URL hits: 1,029
Subscribers: 7
|
|
