Coq tool
The Coq tool is a proof assistant which:
- allows to handle calculus assertions,
- to check mechanically proofs of these assertions,
- helps to find formal proofs,
- extracts a certified program from the constructive proof of its formal specification.
|
Current Version: 6.1
License Type: Freely Available.
|
Home Site:
http://pauillac.inria.fr/coq/systeme_coq-eng.html
Source Code Availability:
Yes
Available Binary Packages:
- Debian Package: No
- RedHat RPM Package: No
- Other Packages: No
Targeted Platforms:
Unix
Software/Hardware Requirements:
Coq is written in the Objective Caml language and thus you need the Objective Caml compiler in order to install
Coq on your system.
|
Other Links:
Proof General
Mailing Lists/USENET News Groups:
To join the mailing list coq-club@pauillac.inria.fr, drop a note to
coq-club-request@pauillac.inria.fr
User Comments:
See A Screen Shot? (Not Yet)
|