1 files changed, 101 insertions, 1 deletions
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index d9eaa2c6c6..ac6f30ceda 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -45,6 +45,54 @@ s},
   year        = {1972}
 }
 
+@inproceedings{CH85,
+  title={Constructions: a higher order proof system for mechanizing mathematics},
+  author={Coquand, Thierry and Huet, Gerard},
+  booktitle={European Conference on Computer Algebra},
+  pages={151--184},
+  year={1985},
+  organization={Springer}
+}
+
+@techreport{CH88
+  TITLE = {{The calculus of constructions}},
+  AUTHOR = {Coquand, T. and Huet, G{\'e}rard},
+  URL = {https://hal.inria.fr/inria-00076024},
+  NUMBER = {RR-0530},
+  INSTITUTION = {{INRIA}},
+  YEAR = {1986},
+  MONTH = May,
+  PDF = {https://hal.inria.fr/inria-00076024/file/RR-0530.pdf},
+  HAL_ID = {inria-00076024},
+  HAL_VERSION = {v1},
+}
+
+@techreport{CH87,
+  TITLE = {{Concepts mathematiques et informatiques formalises dans le calcul des constructions}},
+  AUTHOR = {Coquand, T. and Huet, G{\'e}rard},
+  URL = {https://hal.inria.fr/inria-00076039},
+  NUMBER = {RR-0515},
+  INSTITUTION = {{INRIA}},
+  YEAR = {1986},
+  MONTH = Apr,
+  PDF = {https://hal.inria.fr/inria-00076039/file/RR-0515.pdf},
+  HAL_ID = {inria-00076039},
+  HAL_VERSION = {v1},
+}
+
+@techreport{C90,
+  TITLE = {{Metamathematical investigations of a calculus of constructions}},
+  AUTHOR = {Coquand, T.},
+  URL = {https://hal.inria.fr/inria-00075471},
+  NUMBER = {RR-1088},
+  INSTITUTION = {{INRIA}},
+  YEAR = {1989},
+  MONTH = Sep,
+  PDF = {https://hal.inria.fr/inria-00075471/file/RR-1088.pdf},
+  HAL_ID = {inria-00075471},
+  HAL_VERSION = {v1},
+}
+
 @PhDThesis{Coq85,
   author      = {Th. Coquand},
   month       = jan,
@@ -80,6 +128,15 @@ s},
   bibsource = {DBLP, http://dblp.uni-trier.de}
 }
 
+@inproceedings{CP90,
+  title={Inductively defined types},
+  author={Coquand, Thierry and Paulin, Christine},
+  booktitle={COLOG-88},
+  pages={50--66},
+  year={1990},
+  organization={Springer}
+}
+
 @Book{Cur58,
   author      = {Haskell B. Curry and Robert Feys and William Craig},
   title       = {Combinatory Logic},
@@ -216,7 +273,15 @@ s},
   year        = {1980}
 }
 
-@InProceedings{Hue88,
+@inproceedings{H88,
+  title={Induction principles formalized in the Calculus of Constructions},
+  author={Huet, G{\'e}rard},
+  booktitle={Programming of Future Generation Computers. Elsevier Science},
+  year={1988},
+  organization={Citeseer}
+}
+
+@InProceedings{H89,
   author      = {G. Huet},
   booktitle   = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
   editor      = {R. Narasimhan},
@@ -305,6 +370,41 @@ s},
   url       = {http://www.xmailserver.org/diff2.pdf}
 }
 
+@inproceedings{P86,
+  title={Algorithm development in the calculus of constructions},
+  author={Mohring, Christine},
+  booktitle={LICS},
+  pages={84--91},
+  year={1986}
+}
+
+@inproceedings{P89,
+  title={Extracting $\Omega$'s programs from proofs in the calculus of constructions},
+  author={Paulin-Mohring, Christine},
+  booktitle={Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
+  pages={89--104},
+  year={1989},
+  organization={ACM}
+}
+
+@inproceedings{P93,
+  title={Inductive definitions in the system coq rules and properties},
+  author={Paulin-Mohring, Christine},
+  booktitle={International Conference on Typed Lambda Calculi and Applications},
+  pages={328--345},
+  year={1993},
+  organization={Springer}
+}
+
+@inproceedings{PP90,
+  title={Inductively defined types in the Calculus of Constructions},
+  author={Pfenning, Frank and Paulin-Mohring, Christine},
+  booktitle={International Conference on Mathematical Foundations of Programming Semantics},
+  pages={209--228},
+  year={1989},
+  organization={Springer}
+}
+
 @InProceedings{Parent95b,
   author      = {C. Parent},
   booktitle   = {{Mathematics of Program Construction'95}},