From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- dev/doc/README-V1-V5 | 296 --------------------------------------------------- 1 file changed, 296 deletions(-) delete mode 100644 dev/doc/README-V1-V5 (limited to 'dev/doc/README-V1-V5') diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5 deleted file mode 100644 index ebbc0577..00000000 --- a/dev/doc/README-V1-V5 +++ /dev/null @@ -1,296 +0,0 @@ - - Notes on the prehistory of Coq - -This document is a copy within the Coq archive of a document written -in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin -to accompany their public release of the archive of versions 1.10 to 6.2 -of Coq and of its CONSTR ancestor. 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. -- cgit v1.2.3