Merge PR #9133: Move README-V1-V5 to credits chapter

Reviewed-by: cpitclaudel

1 files changed, 0 insertions, 378 deletions

diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc
deleted file mode 100644
index 631fb92c97..0000000000
--- a/dev/doc/README-V1-V5.asciidoc
+++ /dev/null
@@ -1,378 +0,0 @@
-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 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) 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__ <<CH85>>.
-
-Christine Paulin joined the team at this point, for her DEA research
-internship.  In her DEA memoir (August 1985) she presents developments
-for the _lambo_ function – _lambo(f)(n)_ computes the minimal _m_ such
-that _f(m)_ is greater than _n_, for _f_ an increasing integer
-function, a challenge for constructive mathematics. She also encoded
-the majority voting algorithm of Boyer and Moore.
-
-Version 2
----------
-
-The formal system, now renamed as the _Calculus of Constructions_, was
-presented with a proof of consistency and comparisons with proof
-systems of Per Martin Löf, Girard, and the Automath family of N. de
-Bruijn, in the paper: T. Coquand and G. Huet. __The Calculus of
-Constructions__ <<CH88>>.
-
-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__<<CH87>>.
-
-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__ <<P86>>. 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__ <<H88>>.
-
-Version 3
----------
-
-This version saw the beginning of proof automation, with a search
-algorithm inspired from PROLOG and the applicative logic programming
-programs of the course notes _Formal structures for computation and
-deduction_.  The search algorithm was implemented in ML by Thierry
-Coquand.  The proof system could thus be used in two modes: proof
-verification and proof synthesis, with tactics such as `AUTO`.
-
-The implementation language was now called CAML, for Categorical
-Abstract Machine Language. It used as backend the LLM3 virtual machine
-of Le Lisp by Jérôme Chailloux. The main developers of CAML were
-Michel Mauny, Ascander Suarez and Pierre Weis.
-
-V3.1 was started in the summer of 1986, V3.2 was frozen at the end of
-November 1986. V3.4 was developed in the first half of 1987.
-
-Thierry Coquand held a post-doctoral position in Cambrige University
-in 1986-87, where he developed a variant implementation in SML, with
-which he wrote some developments on fixpoints in Scott's domains.
-
-Version 4
----------
-
-This version saw the beginning of program extraction from proofs, with
-two varieties of the type `Prop` of propositions, indicating
-constructive intent.  The proof extraction algorithms were implemented
-by Christine Paulin-Mohring.
-
-V4.1 was frozen on July 24th, 1987. It had a first identified library
-of mathematical developments (directory exemples), with libraries
-Logic (containing impredicative encodings of intuitionistic logic and
-algebraic primitives for booleans, natural numbers and list), `Peano`
-developing second-order Peano arithmetic, `Arith` defining addition,
-multiplication, euclidean division and factorial. Typical developments
-were the Knaster-Tarski theorem and Newman's lemma from rewriting
-theory.
-
-V4.2 was a joint development of a team consisting of Thierry Coquand,
-Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the
-log of changes.  It was frozen on September 1987 as the last version
-implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable
-development system.
-
-V4.3 saw the first top-level of the system. Instead of evaluating
-explicit quotations, the user could develop his mathematics in a
-high-level language called the mathematical vernacular (following
-Automath terminology).  The user could develop files in the vernacular
-notation (with .v extension) which were now separate from the `ml`
-sources of the implementation.  Gilles Dowek joined the team to
-develop the vernacular language as his DEA internship research.
-
-A notion of sticky constant was introduced, in order to keep names of
-lemmas when local hypotheses of proofs were discharged. This gave a
-notion of global mathematical environment with local sections.
-
-Another significant practical change was that the system, originally
-developped on the VAX central computer of our lab, was transferred on
-SUN personal workstations, allowing a level of distributed
-development.  The extraction algorithm was modified, with three
-annotations `Pos`, `Null` and `Typ` decorating the sorts `Prop` and
-`Type`.
-
-Version 4.3 was frozen at the end of November 1987, and was
-distributed to an early community of users (among those were Hugo
-Herbelin and Loic Colson).
-
-V4.4 saw the first version of (encoded) inductive types.  Now natural
-numbers could be defined as:
-
-[source, coq]
-Inductive NAT : Prop = O : NAT | Succ : NAT->NAT.
-
-These inductive types were encoded impredicatively in the calculus,
-using a subsystem _rec_ due to Christine Paulin.  V4.4 was frozen on
-March 6th 1988.
-
-Version 4.5 was the first one to support inductive types and program
-extraction.  Its banner was _Calcul des Constructions avec
-Réalisations et Synthèse_.  The vernacular language was enriched to
-accommodate extraction commands.
-
-The verification engine design was presented as: G. Huet. _The
-Constructive Engine_. Version 4.5. Invited Conference, 2nd European
-Symposium on Programming, Nancy, March 88.  The final paper,
-describing the V4.9 implementation, appeared in: A perspective in
-Theoretical Computer Science, Commemorative Volume in memory of Gift
-Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989.
-
-Version 4.5 was demonstrated in June 1988 at the YoP Institute on
-Logical Foundations of Functional Programming organized by Gérard Huet
-at Austin, Texas.
-
-Version 4.6 was started during the summer of 1988. Its main
-improvement was the complete rehaul of the proof synthesis engine by
-Thierry Coquand, with a tree structure of goals.
-
-Its source code was communicated to Randy Pollack on September 2nd
-1988.  It evolved progressively into LEGO, proof system for Luo's
-formalism of Extended Calculus of Constructions.
-
-The discharge tactic was modified by Gérard Huet to allow for
-inter-dependencies in discharged lemmas. Christine Paulin improved the
-inductive definition scheme in order to accommodate predicates of any
-arity.
-
-Version 4.7 was started on September 6th, 1988.
-
-This version starts exploiting the CAML notion of module in order to
-improve the modularity of the implementation. Now the term verifier is
-identified as a proper module Machine, which the structure of its
-internal data structures being hidden and thus accessible only through
-the legitimate operations.  This machine (the constructive engine) was
-the trusted core of the implementation. The proof synthesis mechanism
-was a separate proof term generator. Once a complete proof term was
-synthesized with the help of tactics, it was entirely re-checked by
-the engine. Thus there was no need to certify the tactics, and the
-system took advantage of this fact by having tactics ignore the
-universe levels, universe consistency check being relegated to the
-final type-checking pass. This induced a certain puzzlement in early
-users who saw, after a successful proof search, their `QED` followed
-by silence, followed by a failure message due to a universe
-inconsistency…
-
-The set of examples comprise set theory experiments by Hugo Herbelin,
-and notably the Schroeder-Bernstein theorem.
-
-Version 4.8, started on October 8th, 1988, saw a major
-re-implementation of the abstract syntax type `constr`, separating
-variables of the formalism and metavariables denoting incomplete terms
-managed by the search mechanism.  A notion of level (with three values
-`TYPE`, `OBJECT` and `PROOF`) is made explicit and a type judgement
-clarifies the constructions, whose implementation is now fully
-explicit. Structural equality is speeded up by using pointer equality,
-yielding spectacular improvements. Thierry Coquand adapts the proof
-synthesis to the new representation, and simplifies pattern matching
-to first-order predicate calculus matching, with important performance
-gain.
-
-A new representation of the universe hierarchy is then defined by
-Gérard Huet.  Universe levels are now implemented implicitly, through
-a hidden graph of abstract levels constrained with an order relation.
-Checking acyclicity of the graph insures well-foundedness of the
-ordering, and thus consistency. This was documented in a memo _Adding
-Type:Type to the Calculus of Constructions_ which was never published.
-
-The development version is released as a stable 4.8 at the end of
-1988.
-
-Version 4.9 is released on March 1st 1989, with the new ``elastic''
-universe hierarchy.
-
-The spring of 1989 saw the first attempt at documenting the system
-usage, with a number of papers describing the formalism:
-
-- _Metamathematical Investigations of a Calculus of Constructions_, by
-  Thierry Coquand <<C90>>,
-- _Inductive definitions in the Calculus of Constructions_, by
-   Christine Paulin-Mohrin,
-- _Extracting Fω's programs from proofs in the Calculus of
-  Constructions_, by Christine Paulin-Mohring <<P89>>,
-- _The Constructive Engine_, by Gérard Huet <<H89>>,
-
-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__ <<PP90>>. An extension of the calculus
-with primitive inductive types appeared in: Th. Coquand and
-C. Paulin-Mohring. __Inductively defined types__ <<CP90>>.
-
-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__ <<P93>>.
-
-The last version of CONSTR is Version 4.11, which was last distributed
-in the spring of 1990. It was demonstrated at the first workshop of
-the European Basic Research Action Logical Frameworks In Sophia
-Antipolis in May 1990.
-
-At the end of 1989, Version 5.1 was started, and renamed as the system
-Coq for the Calculus of Inductive Constructions. It was then ported to
-the new stand-alone implementation of ML called Caml-light.
-
-In 1990 many changes occurred. Thierry Coquand left for Chalmers
-University in Göteborg. Christine Paulin-Mohring took a CNRS
-researcher position at the LIP laboratory of École Normale Supérieure
-de Lyon. Project Formel was terminated, and gave rise to two teams:
-Cristal at INRIA-Roquencourt, that continued developments in
-functional programming with Caml-light then Ocaml, and Coq, continuing
-the type theory research, with a joint team headed by Gérard Huet at
-INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory
-of CNRS-ENS Lyon.
-
-Chetan Murthy joined the team in 1991 and became the main software
-architect of Version 5. He completely rehauled the implementation for
-efficiency.  Versions 5.6 and 5.8 were major distributed versions,
-with complete documentation and a library of users' developements. The
-use of the RCS revision control system, and systematic ChangeLog
-files, allow a more precise tracking of the software developments.
-
-Developments from Version 6 upwards are documented in the credits
-section of Coq's Reference Manual.
-
-====
-September 2015 +
-Thierry Coquand, Gérard Huet and Christine Paulin-Mohring.
-====
-
-[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.