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 is the beta version of a new major evolution
of the Coq system. Its features include a more
extensible logical system, a completely new syntax
of terms, a slightly revised syntax for tactics
and commands, a smart and robust
comment-preserving automatic translator from old
to 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.
