| Other Scientific Fields
| Artificial Intelligence
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.
Source Code Availability:
Available Binary Packages:
- Debian Package: No
- RedHat RPM Package: No
- Other Packages: No
Coq is written in the Objective Caml language and thus you need the Objective Caml compiler in order to install
Coq on your system.
Mailing Lists/USENET News Groups:
To join the mailing list firstname.lastname@example.org, drop a note to
See A Screen Shot? (Not Yet)
Copyright © 1995-2001 by
Copyright © 1997-2001 by
Kachina Technologies, Inc.
All rights reserved.