CMU Artificial Intelligence Repository
Coq: Calculus of Inductive Constructions
areas/reasonng/atp/systems/coq/
This directory contains Coq, the Calculus of Inductive Constructions.
See Also:
lang/others/ml/caml_lt/
Origin:
ftp.inria.fr:/INRIA/coq/V5.8.3 (unix version)
ftp.inria.fr:/INRIA/coq/V5.8.2 (mac version)
Version: Unix 5.8.3 (6-DEC-93); Mac 5.8.2 (8-JUL-93)
Requires: Caml-Light, C, X11
The Mac version is standalone, not requiring Caml-Light.
The unix version requires Caml-Light.
Ports: Unix, Macintosh
CD-ROM: Prime Time Freeware for AI, Issue 1-1
Contact: Coq hotline .
Keywords:
Automated Reasoning, Coq, ML!Code,
Reasoning!Automated Reasoning, Theorem Proving
References:
Documentation is included in the distribution.
Last Web update on Mon Feb 13 10:27:27 1995
AI.Repository@cs.cmu.edu