diff options
| -rwxr-xr-x | doc/biblio.bib | 40 |
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}, |