Ajout r�f�rences Alexandre Miquel

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8597 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 39 insertions, 1 deletions

diff --git a/doc/biblio.bib b/doc/biblio.bib
index 1c0a6eab3a..9962d5c57b 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -152,7 +152,7 @@ s},
 @TECHREPORT{COQ02,
         AUTHOR             = {The Coq Development Team},
         INSTITUTION        = {INRIA},
-        MONTH              = February,
+        MONTH              = Feb,
         NUMBER             = {255},
         TITLE              = {{The Coq Proof Assistant Reference Manual Version 7.2}},
         YEAR               = {2002}
@@ -776,6 +776,44 @@ of the {ML} language},
         YEAR               = {To appear}
 }
 
+@INPROCEEDINGS{Miquel00,
+        AUTHOR             = {A. Miquel},
+        TITLE              = {A Model for Impredicative Type Systems with Universes,
+Intersection Types and Subtyping},
+        BOOKTITLE          = {{Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00)}},
+        PUBLISHER          = {IEEE Computer Society Press},
+        YEAR               = {2000}
+}
+
+@PHDTHESIS{Miquel01a,
+        AUTHOR             = {A. Miquel},
+        TITLE              = {Le Calcul des Constructions implicite: syntaxe et s\'emantique},
+        MONTH              = {dec},
+        SCHOOL             = {{Universit\'e Paris 7}},
+        YEAR               = {2001}
+}
+
+@INPROCEEDINGS{Miquel01b,
+        AUTHOR             = {A. Miquel},
+        TITLE              = {The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping},
+        BOOKTITLE          = {{Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA01), Krakow, Poland}},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        NUMBER             = 2044,
+        YEAR               = {2001}
+}
+
+@INPROCEEDINGS{MiWer02,
+        AUTHOR             = {A. Miquel and B. Werner},
+        TITLE              = {The Not So Simple Proof-Irrelevant Model of CC},
+        BOOKTITLE          = {Types for Proofs and Programs (TYPES'02)},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        NUMBER             = 2646,
+        YEAR               = 2003
+}
+
+
 @INPROCEEDINGS{Moh89a,
         AUTHOR             = {C. Paulin-Mohring},
         ADDRESS            = {Austin},