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: None See A Screen Shot? (Not Yet)

  SAL Home   |   Other Scientific Fields   |   Artificial Intelligence