From 5357b9849bd6eb0be4f8d60b4e1c091ad5167932 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 5 Nov 2015 19:43:44 +0100 Subject: Prehistory of Coq: asciidoc conversion. Formatting markup + typography. --- dev/doc/README-V1-V5 | 293 --------------------------------------- dev/doc/README-V1-V5.asciidoc | 312 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 312 insertions(+), 293 deletions(-) delete mode 100644 dev/doc/README-V1-V5 create mode 100644 dev/doc/README-V1-V5.asciidoc (limited to 'dev') diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5 deleted file mode 100644 index 2ca62e3d74..0000000000 --- a/dev/doc/README-V1-V5 +++ /dev/null @@ -1,293 +0,0 @@ - - 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. diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc new file mode 100644 index 0000000000..f6ee27d486 --- /dev/null +++ b/dev/doc/README-V1-V5.asciidoc @@ -0,0 +1,312 @@ +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) +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 (λ) +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 +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: + +[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 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 first-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 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 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 É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. +==== \ No newline at end of file -- cgit v1.2.3 From e82fc7cb4104d28619448bde374afde7e32f3dc2 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 6 Nov 2015 09:15:47 +0100 Subject: Prehistory of Coq: various corrections on English. --- dev/doc/README-V1-V5.asciidoc | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) (limited to 'dev') diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc index f6ee27d486..43971ba553 100644 --- a/dev/doc/README-V1-V5.asciidoc +++ b/dev/doc/README-V1-V5.asciidoc @@ -25,10 +25,10 @@ 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 +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. @@ -47,10 +47,11 @@ Th. Coquand, G. Huet. _Constructions: A Higher Order Proof System for Mechanizin 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 +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 @@ -185,7 +186,7 @@ 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 +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. @@ -209,9 +210,9 @@ 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… +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. @@ -238,7 +239,7 @@ 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, +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 @@ -272,7 +273,7 @@ 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 +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 @@ -280,7 +281,7 @@ 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 +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 -- cgit v1.2.3 From bbfa17765599a04931efa68a5397f418e6ea5b39 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 6 Nov 2015 09:18:54 +0100 Subject: Prehistory of Coq: consistency. Don't use abbreviated first names in sentences. --- dev/doc/README-V1-V5.asciidoc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dev') diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc index 43971ba553..a02f0831dc 100644 --- a/dev/doc/README-V1-V5.asciidoc +++ b/dev/doc/README-V1-V5.asciidoc @@ -194,7 +194,7 @@ 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 +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. @@ -227,7 +227,7 @@ 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. Huet. +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, -- cgit v1.2.3 From 856e746e2a0adf959faee0907555af81be11d027 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 6 Nov 2015 09:26:50 +0100 Subject: Prehistory of Coq: justification of the plain text. --- dev/doc/README-V1-V5.asciidoc | 483 ++++++++++++++++++++++-------------------- 1 file changed, 254 insertions(+), 229 deletions(-) (limited to 'dev') diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc index a02f0831dc..4395fd0e5c 100644 --- a/dev/doc/README-V1-V5.asciidoc +++ b/dev/doc/README-V1-V5.asciidoc @@ -8,44 +8,47 @@ Notes on the prehistory of Coq :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. +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. +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 @@ -57,255 +60,277 @@ 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. +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. +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. +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. +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. +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 +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. +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`. +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. +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. +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. +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: +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. +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… +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.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: +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) + 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) + 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. +- _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 +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. +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. +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. +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 + -- cgit v1.2.3 From fd7eb1dd0f2cf5fab3a6a2a5f567acaca2defed5 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 11 Nov 2015 00:02:21 +0100 Subject: Prehistory of Coq: move the bibliographic references to a dedicated section. So as not to clutter the text. Also took the opportunity to add a few missing references. --- dev/doc/README-V1-V5.asciidoc | 121 +++++++++++++++++++++++++++--------------- 1 file changed, 79 insertions(+), 42 deletions(-) (limited to 'dev') diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc index 4395fd0e5c..9a4261b3a7 100644 --- a/dev/doc/README-V1-V5.asciidoc +++ b/dev/doc/README-V1-V5.asciidoc @@ -45,10 +45,8 @@ 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. +for the examples in the paper: Th. Coquand, G. Huet. __Constructions: A +Higher Order Proof System for Mechanizing Mathematics__ <>. Christine Paulin joined the team at this point, for her DEA research internship. In her DEA memoir (August 1985) she presents developments @@ -63,19 +61,14 @@ 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. +Bruijn, in the paper: T. Coquand and G. Huet. __The Calculus of +Constructions__ <>. 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 +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. +Constructions__<>. Version 2.8 was frozen on December 16th, 1985, and served for developing the exemples in the above papers. @@ -86,12 +79,9 @@ 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. +Christine Paulin wrote an article __Algorithm development in the +Calculus of Constructions__ <>. 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. @@ -102,9 +92,8 @@ 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. +as __Induction Principles Formalized in the Calculus of +Constructions__ <>. Version 3 --------- @@ -263,14 +252,12 @@ 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) + Thierry Coquand <>, - _Inductive definitions in the Calculus of Constructions_, by - Christine Paulin-Mohring, + Christine Paulin-Mohrin, - _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 + Constructions_, by Christine Paulin-Mohring <>, +- _The Constructive Engine_, by Gérard Huet <>, as well as a number of user guides: @@ -286,22 +273,15 @@ 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. +F. Pfenning and C. Paulin-Mohring. __Inductively defined types in the +Calculus of Constructions__ <>. An extension of the calculus +with primitive inductive types appeared in: Th. Coquand and +C. Paulin-Mohring. __Inductively defined types__ <>. 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. +C. Paulin-Mohring. __Inductive Definitions in the System Coq - Rules +and Properties__ <>. 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 @@ -335,4 +315,61 @@ section of Coq's Reference Manual. ==== September 2015 + Thierry Coquand, Gérard Huet and Christine Paulin-Mohring. -==== \ No newline at end of file +==== + +[bibliography] +.Bibliographic references + +- [[[CH85]]] 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. + +- [[[CH88]]] 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. + +- [[[CH87]]] 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. + +- [[[P86]]] C. Paulin. _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). + +- [[[H88]]] G. Huet. _Induction Principles Formalized in the Calculus + of Constructions_ in Programming of Future Generation Computers, + Ed. K. Fuchi and M. Nivat, North-Holland, 1988. + +- [[[C90]]] Th. Coquand. _Metamathematical Investigations of a + Calculus of Constructions_, by INRIA Research Report N°1088, + Sept. 1989, published in Logic and Computer Science, + ed. P.G. Odifreddi, Academic Press, 1990. + +- [[[P89]]] C. Paulin. _Extracting F ω's programs from proofs in the + calculus of constructions_. 16th Annual ACM Symposium on Principles + of Programming Languages, Austin. 1989. + +- [[[H89]]] G. Huet. _The constructive engine_. A perspective in + Theoretical Computer Science. Commemorative Volume for Gift + Siromoney. World Scientific Publishing (1989). + +- [[[PP90]]] 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 + +- [[[CP90]]] 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. + +- [[[P93]]] 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. -- cgit v1.2.3