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.
Information regarding Project Releases and Project Resources. Note that the information here is a quote from Freecode.com page, and the downloads themselves may not be hosted on OSDN.
This release brings Haskell-style type classes, various evolutions of the arithmetic libraries, and many other various improvements and extensions regarding the module system, tactics, syntax, etc.
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).
This is a new major evolution of the Coq system. It features a more extensible logical system due to the removal of the impredicativity of the sort Set, a completely new syntax, an automatic translator from the old to the new syntax, a new notion of "interpretation scopes", a revised and simplified standard library, a new automation tactic for first-order statements, and a new integrated GTK-based user interface.