diff options
Diffstat (limited to 'dev/doc/README-V1-V5')
-rw-r--r-- | dev/doc/README-V1-V5 | 293 |
1 files changed, 293 insertions, 0 deletions
diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5 new file mode 100644 index 00000000..2ca62e3d --- /dev/null +++ b/dev/doc/README-V1-V5 @@ -0,0 +1,293 @@ + + Notes on the prehistory of Coq + +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 Ecole 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) +is a version of ML issued from the Edinburgh LCF system and running on +a LISP backend. The main improvements from the original LCF ML are that ML +is compiled rather than interpreted (Gérard Huet building on the original +translator by Lockwood Morris), and that it is 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 (lambda) +at the level of terms/proofs, in the manner of Automath. Substitution +(lambda 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 +computing 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: +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 Realisations et Synthese". +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 summer 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. 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 of early users who saw +their successful proof search ended with QED, followed by silence, followed by +a failure message of universe inconsistency rejection... + +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 1st order +predicate calculus matching, with important performance gain. + +A new representation of the universe hierarchy is then defined by G. 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 89 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 Fomega'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 lead 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 Spring 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 Ecole 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. |