path: root/dev/doc/README-V1-V5.asciidoc

Notes on the prehistory of Coq
==============================
:author:  Thierry Coquand, Gérard Huet & Christine Paulin-Mohring
:revdate: September 2015
:toc:
:toc-placement: preamble
:toclevels: 1
:showtitle:


This archive contains the sources of the CONSTR ancestor of the Coq
proof assistant. CONSTR, then Coq, was designed and implemented in the
Formel team, joint between the INRIA Rocquencourt laboratory and the
École Normale Supérieure of Paris, from 1984 onwards.

Version 1
---------

This software is a prototype type-checker for a higher-order logical
formalism known as the Theory of Constructions, presented in his PhD
thesis by Thierry Coquand, with influences from Girard's system F and
de Bruijn's Automath.  The metamathematical analysis of the system is
the PhD work of Thierry Coquand. The software is mostly the work of
Gérard Huet.  Most of the mathematical examples verified with the
software are due to Thierry Coquand.

The programming language of the CONSTR software (as it was called at
the time) was a version of ML adapted from the Edinburgh LCF system
and running on a LISP backend. The main improvements from the original
LCF ML were that ML was compiled rather than interpreted (Gérard Huet
building on the original translator by Lockwood Morris), and that it
was enriched by recursively defined types (work of Guy
Cousineau). This ancestor of CAML was used and improved by Larry
Paulson for his implementation of Cambridge LCF.

Software developments of this prototype occurred from late 1983 to
early 1985.

Version 1.10 was frozen on December 22nd 1984. It is the version used
for the examples in Thierry Coquand's thesis, defended on January 31st
1985.  There was a unique binding operator, used both for universal
quantification (dependent product) at the level of types and
functional abstraction (λ) at the level of terms/proofs, in the manner
of Automath. Substitution (λ-reduction) was implemented using de
Bruijn's indexes.

Version 1.11 was frozen on February 19th, 1985. It is the version used
for the examples in the paper: Th. Coquand, G. Huet. _Constructions: A
Higher Order Proof System for Mechanizing Mathematics_. Invited paper,
EUROCAL85, April 1985, Linz, Austria. Springer Verlag LNCS 203,
pp. 151-184.

Christine Paulin joined the team at this point, for her DEA research
internship.  In her DEA memoir (August 1985) she presents developments
for the _lambo_ function – _lambo(f)(n)_ computes the minimal _m_ such
that _f(m)_ is greater than _n_, for _f_ an increasing integer
function, a challenge for constructive mathematics. She also encoded
the majority voting algorithm of Boyer and Moore.

Version 2
---------

The formal system, now renamed as the _Calculus of Constructions_, was
presented with a proof of consistency and comparisons with proof
systems of Per Martin Löf, Girard, and the Automath family of N. de
Bruijn, in the paper: T. Coquand and G. Huet. _The Calculus of
Constructions_.  Submitted on June 30th 1985, accepted on December
5th, 1985, Information and Computation. Preprint as Rapport de
Recherche Inria n°530, Mai 1986. Final version in Information and
Computation 76,2/3, Feb. 88.

An abstraction of the software design, in the form of an abstract
machine for proof checking, and a fuller sequence of mathematical
developments was presented in: Th. Coquand, G. Huet. _Concepts
Mathématiques et Informatiques Formalisés dans le Calcul des
Constructions_. Invited paper, European Logic Colloquium, Orsay, July
1985. Preprint as Rapport de recherche INRIA n°463, Dec. 85.
Published in Logic Colloquium 1985, North-Holland, 1987.

Version 2.8 was frozen on December 16th, 1985, and served for
developing the exemples in the above papers.

This calculus was then enriched in version 2.9 with a cumulative
hierarchy of universes. Universe levels were initially explicit
natural numbers.  Another improvement was the possibility of automatic
synthesis of implicit type arguments, relieving the user of tedious
redundant declarations.

Christine Paulin wrote an article _Algorithm development in the
Calculus of Constructions_, preprint as Rapport de recherche INRIA
n°497, March 86.  Final version in Proceedings Symposium on Logic in
Computer Science, Cambridge, MA, 1986 (IEEE Computer Society
Press). Besides _lambo_ and _majority_, she presents quicksort and a
text formatting algorithm.

Version 2.13 of the Calculus of Constructions with universes was
frozen on June 25th, 1986.

A synthetic presentation of type theory along constructive lines with
ML algorithms was given by Gérard Huet in his May 1986 CMU course
notes _Formal Structures for Computation and Deduction_. Its chapter
_Induction and Recursion in the Theory of Constructions_ was presented
as an invited paper at the Joint Conference on Theory and Practice of
Software Development TAPSOFT’87 at Pise in March 1987, and published
as _Induction Principles Formalized in the Calculus of Constructions_
in Programming of Future Generation Computers, Ed. K. Fuchi and
M. Nivat, North-Holland, 1988.

Version 3
---------

This version saw the beginning of proof automation, with a search
algorithm inspired from PROLOG and the applicative logic programming
programs of the course notes _Formal structures for computation and
deduction_.  The search algorithm was implemented in ML by Thierry
Coquand.  The proof system could thus be used in two modes: proof
verification and proof synthesis, with tactics such as `AUTO`.

The implementation language was now called CAML, for Categorical
Abstract Machine Language. It used as backend the LLM3 virtual machine
of Le Lisp by Jérôme Chailloux. The main developers of CAML were
Michel Mauny, Ascander Suarez and Pierre Weis.

V3.1 was started in the summer of 1986, V3.2 was frozen at the end of
November 1986. V3.4 was developed in the first half of 1987.

Thierry Coquand held a post-doctoral position in Cambrige University
in 1986-87, where he developed a variant implementation in SML, with
which he wrote some developments on fixpoints in Scott's domains.

Version 4
---------

This version saw the beginning of program extraction from proofs, with
two varieties of the type `Prop` of propositions, indicating
constructive intent.  The proof extraction algorithms were implemented
by Christine Paulin-Mohring.

V4.1 was frozen on July 24th, 1987. It had a first identified library
of mathematical developments (directory exemples), with libraries
Logic (containing impredicative encodings of intuitionistic logic and
algebraic primitives for booleans, natural numbers and list), `Peano`
developing second-order Peano arithmetic, `Arith` defining addition,
multiplication, euclidean division and factorial. Typical developments
were the Knaster-Tarski theorem and Newman's lemma from rewriting
theory.

V4.2 was a joint development of a team consisting of Thierry Coquand,
Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the
log of changes.  It was frozen on September 1987 as the last version
implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable
development system.

V4.3 saw the first top-level of the system. Instead of evaluating
explicit quotations, the user could develop his mathematics in a
high-level language called the mathematical vernacular (following
Automath terminology).  The user could develop files in the vernacular
notation (with .v extension) which were now separate from the `ml`
sources of the implementation.  Gilles Dowek joined the team to
develop the vernacular language as his DEA internship research.

A notion of sticky constant was introduced, in order to keep names of
lemmas when local hypotheses of proofs were discharged. This gave a
notion of global mathematical environment with local sections.

Another significant practical change was that the system, originally
developped on the VAX central computer of our lab, was transferred on
SUN personal workstations, allowing a level of distributed
development.  The extraction algorithm was modified, with three
annotations `Pos`, `Null` and `Typ` decorating the sorts `Prop` and
`Type`.

Version 4.3 was frozen at the end of November 1987, and was
distributed to an early community of users (among those were Hugo
Herbelin and Loic Colson).

V4.4 saw the first version of (encoded) inductive types.  Now natural
numbers could be defined as:

[source, coq]
Inductive NAT : Prop = O : NAT | Succ : NAT->NAT.

These inductive types were encoded impredicatively in the calculus,
using a subsystem _rec_ due to Christine Paulin.  V4.4 was frozen on
March 6th 1988.

Version 4.5 was the first one to support inductive types and program
extraction.  Its banner was _Calcul des Constructions avec
Réalisations et Synthèse_.  The vernacular language was enriched to
accommodate extraction commands.

The verification engine design was presented as: G. Huet. _The
Constructive Engine_. Version 4.5. Invited Conference, 2nd European
Symposium on Programming, Nancy, March 88.  The final paper,
describing the V4.9 implementation, appeared in: A perspective in
Theoretical Computer Science, Commemorative Volume in memory of Gift
Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989.

Version 4.5 was demonstrated in June 1988 at the YoP Institute on
Logical Foundations of Functional Programming organized by Gérard Huet
at Austin, Texas.

Version 4.6 was started during the summer of 1988. Its main
improvement was the complete rehaul of the proof synthesis engine by
Thierry Coquand, with a tree structure of goals.

Its source code was communicated to Randy Pollack on September 2nd
1988.  It evolved progressively into LEGO, proof system for Luo's
formalism of Extended Calculus of Constructions.

The discharge tactic was modified by Gérard Huet to allow for
inter-dependencies in discharged lemmas. Christine Paulin improved the
inductive definition scheme in order to accommodate predicates of any
arity.

Version 4.7 was started on September 6th, 1988.

This version starts exploiting the CAML notion of module in order to
improve the modularity of the implementation. Now the term verifier is
identified as a proper module Machine, which the structure of its
internal data structures being hidden and thus accessible only through
the legitimate operations.  This machine (the constructive engine) was
the trusted core of the implementation. The proof synthesis mechanism
was a separate proof term generator. Once a complete proof term was
synthesized with the help of tactics, it was entirely re-checked by
the engine. Thus there was no need to certify the tactics, and the
system took advantage of this fact by having tactics ignore the
universe levels, universe consistency check being relegated to the
final type-checking pass. This induced a certain puzzlement in early
users who saw, after a successful proof search, their `QED` followed
by silence, followed by a failure message due to a universe
inconsistency…

The set of examples comprise set theory experiments by Hugo Herbelin,
and notably the Schroeder-Bernstein theorem.

Version 4.8, started on October 8th, 1988, saw a major
re-implementation of the abstract syntax type `constr`, separating
variables of the formalism and metavariables denoting incomplete terms
managed by the search mechanism.  A notion of level (with three values
`TYPE`, `OBJECT` and `PROOF`) is made explicit and a type judgement
clarifies the constructions, whose implementation is now fully
explicit. Structural equality is speeded up by using pointer equality,
yielding spectacular improvements. Thierry Coquand adapts the proof
synthesis to the new representation, and simplifies pattern matching
to first-order predicate calculus matching, with important performance
gain.

A new representation of the universe hierarchy is then defined by
Gérard Huet.  Universe levels are now implemented implicitly, through
a hidden graph of abstract levels constrained with an order relation.
Checking acyclicity of the graph insures well-foundedness of the
ordering, and thus consistency. This was documented in a memo _Adding
Type:Type to the Calculus of Constructions_ which was never published.

The development version is released as a stable 4.8 at the end of
1988.

Version 4.9 is released on March 1st 1989, with the new ``elastic''
universe hierarchy.

The spring of 1989 saw the first attempt at documenting the system
usage, with a number of papers describing the formalism:

- _Metamathematical Investigations of a Calculus of Constructions_, by
  Thierry Coquand (INRIA Research Report N°1088, Sept. 1989, published
  in Logic and Computer Science, ed. P.G. Odifreddi, Academic Press,
  1990)
- _Inductive definitions in the Calculus of Constructions_, by
   Christine Paulin-Mohring,
- _Extracting Fω's programs from proofs in the Calculus of
  Constructions_, by Christine Paulin-Mohring (published in POPL'89)
- _The Constructive Engine_, by Gérard Huet

as well as a number of user guides:

- _A short user's guide for the Constructions_ Version 4.10, by Gérard Huet
- _A Vernacular Syllabus_, by Gilles Dowek.
- _The Tactics Theorem Prover, User's guide_, Version 4.10, by Thierry
  Coquand.

Stable V4.10, released on May 1st, 1989, was then a mature system,
distributed with CAML V2.6.

In the mean time, Thierry Coquand and Christine Paulin-Mohring had
been investigating how to add native inductive types to the Calculus
of Constructions, in the manner of Per Martin-Löf's Intuitionistic
Type Theory. The impredicative encoding had already been presented in:
F. Pfenning and C. Paulin-Mohring. _Inductively defined types in the
Calculus of Constructions_. Preprint technical report CMU-CS-89-209,
final version in Proceedings of Mathematical Foundations of
Programming Semantics, volume 442, Lecture Notes in Computer
Science. Springer-Verlag, 1990.  An extension of the calculus with
primitive inductive types appeared in: Th. Coquand and
C. Paulin-Mohring. _Inductively defined types_.  In P. Martin-Löf and
G. Mints, editors, Proceedings of Colog'88, volume 417, Lecture Notes
in Computer Science. Springer-Verlag, 1990.

This led to the Calculus of Inductive Constructions, logical formalism
implemented in Versions 5 upward of the system, and documented in:
C. Paulin-Mohring. _Inductive Definitions in the System Coq - Rules
and Properties_. In M. Bezem and J.-F. Groote, editors, Proceedings of
the conference Typed Lambda Calculi and Applications, volume 664,
Lecture Notes in Computer Science, 1993.

The last version of CONSTR is Version 4.11, which was last distributed
in the spring of 1990. It was demonstrated at the first workshop of
the European Basic Research Action Logical Frameworks In Sophia
Antipolis in May 1990.

At the end of 1989, Version 5.1 was started, and renamed as the system
Coq for the Calculus of Inductive Constructions. It was then ported to
the new stand-alone implementation of ML called Caml-light.

In 1990 many changes occurred. Thierry Coquand left for Chalmers
University in Göteborg. Christine Paulin-Mohring took a CNRS
researcher position at the LIP laboratory of École Normale Supérieure
de Lyon. Project Formel was terminated, and gave rise to two teams:
Cristal at INRIA-Roquencourt, that continued developments in
functional programming with Caml-light then Ocaml, and Coq, continuing
the type theory research, with a joint team headed by Gérard Huet at
INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory
of CNRS-ENS Lyon.

Chetan Murthy joined the team in 1991 and became the main software
architect of Version 5. He completely rehauled the implementation for
efficiency.  Versions 5.6 and 5.8 were major distributed versions,
with complete documentation and a library of users' developements. The
use of the RCS revision control system, and systematic ChangeLog
files, allow a more precise tracking of the software developments.

Developments from Version 6 upwards are documented in the credits
section of Coq's Reference Manual.

====
September 2015 +
Thierry Coquand, Gérard Huet and Christine Paulin-Mohring.
====