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.

1 files changed, 79 insertions, 42 deletions

diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc
index 4395fd0e5..9a4261b3a 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__ <<CH85>>.
 
 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__ <<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
+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__<<CH87>>.
 
 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__ <<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.
@@ -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__ <<H88>>.
 
 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 <<C90>>,
 - _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 <<P89>>,
+- _The Constructive Engine_, by Gérard Huet <<H89>>,
 
 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__ <<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_. 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__ <<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
@@ -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.