@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Name:  Coq

Keywords:  Calculus of Inductive Constructions, Proof Assistant 

Description: 
   Semantics: Calculus of Inductive Constructions, a non-conservative
extension of the Calculus of Constructions with inductive types.

   Deductive machinery:  Goal-directed tactics theorem-prover, with a set
of predefined tactics, including an Auto tactic which tries to apply
previous lemmas declared as hints.
   Dynamics:  You can mix developments in two interfaces, one tty-like,
the other with X-windows interface, allowing quick application of tactics
by clicking in menus, etc. Undo mechanism. Search of relevant lemmas.
   Persistence: Developments in a high-level language called the Mathematical
Vernacular can be saved in files and replayed. Proof states may be saved 
during a session. Automatic log of proof session available on request.
   Program extraction: The logic mixes a constructive logic and a classical
logic. The system automatically extracts the constructive contents of proofs
as an executable ML program, which may be compiled in our CAML implementation.
This permits the development of programs provably consistent with their
specification. The descriptive sub-language of the Mathematical Vernacular
may be seen as a high-level specification language, combining higher-order
predicate calculus, PROLOG-like predicate definitions, and recursive
functional definitions.

Coq is an implementation of the Calculus of Inductive Constructions, under
development at INRIA Rocquencourt and ENS Lyon.  

Contact persons: Use the Coq hotline coq@margaux.inria.fr for any problem
with Coq. A users mailing list is being set-up for actual users. If you
want to be put on this mailing list, ask Gerard.Huet@inria.fr, 
with a short description of your area of interest.

Pragmatics: Well-adapted to inductive reasoning, powerful type system,
program extraction are the main advantages. Weak in libraries, equality
manipulation. No decision procedure. Currently no modular theories.

Documentation: A 180 pages Reference Manual is available as an INRIA technical
report, and is distributed with the system under dvi and ps forms.

Applications: Main application has been developing specifications for
extracting various sorting and graph-manipulation algorithms. Also
Warshall's algorithm, streams manipulation programs, tautology checker.
Various case-studies have been developed: Schroeder-Berstein theorem,
Tarski's theorem, Higman's lemma, Newman's lemma, Gilbreath's card trick.
All these developments are available with the distribution.

See also
Gerard Huet, Amy Felty, B. Werner, H Herbelin, and Gilles Dowek,
``Presenting the system Coq, version 5.6'',
in Proceedings of the Second Workshop on Logical Frameworks,  Edinburgh 1991
Huet, Plotkin, and Jones (eds.)

Where-to-get-it:

Coq is freely available by ftp as follows:
ftp nuri.inria.fr 
or ftp 128.93.1.26
with Name anonymous and Password your email address.
Then do
binary
cd INRIA/coq
get README
get coq.tar.Z
quit
Now uncompress coq.tar.Z, untar coq, and follow the README instructions.

Resource requirements:
Coq runs in CAML V3.1, also available on the same machine in directory
INRIA/caml/V3.1. Versions are currently available for the following machines:
Sun3, Sun4, Decstation, SONY68k, SONYR3000, Apollo, and Macintosh/AUX.
You need 16Mbytes to run Coq comfortably.
In order to run the X interface, you need X-windows or a close-enough
substitute such as DEC's OpenWindows.

We are presently developing a new version on top of caml-light, a smaller 
and more portable implementation of ML which runs on PC's and Mac's.
Coq-light should be available for Xmas 92.

Date: July 92 
Info-source: Gerard Huet

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%