SAL Home OTHERS Artificial Intelligence

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:

Source Code Availability:


Available Binary Packages:

  • Debian Package: No
  • RedHat RPM Package: No
  • Other Packages: No

Targeted Platforms:


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, drop a note to

User Comments:

  • None

See A Screen Shot? (Not Yet)

  SAL Home   |   Other Scientific Fields   |   Artificial Intelligence

Comments? SAL@KachinaTech.COM
Copyright © 1995-2001 by Herng-Jeng Jou
Copyright © 1997-2001 by Kachina Technologies, Inc.
All rights reserved.