CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

Coq: Calculus of Inductive Constructions

This directory contains Coq, the Calculus of Inductive Constructions.
See Also: 

Origin: (unix version) (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