diff options
Diffstat (limited to 'doc/refman/biblio.bib')
| -rw-r--r-- | doc/refman/biblio.bib | 82 |
1 files changed, 48 insertions, 34 deletions
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib index b9a3a2c5..d16c82c5 100644 --- a/doc/refman/biblio.bib +++ b/doc/refman/biblio.bib @@ -100,26 +100,25 @@ Computer Architecture}, YEAR = {1992} } -@inproceedings{Bou97, - title = {Using reflection to build efficient and certified decision procedure +@INPROCEEDINGS{Bou97, + TITLE = {Using reflection to build efficient and certified decision procedure s}, - author = {S. Boutin}, - booktitle = {TACS'97}, - editor = {Martin Abadi and Takahashi Ito}, - publisher = SV, - series = lncs, - volume=1281, - PS={http://pauillac.inria.fr/~boutin/public_w/submitTACS97.ps.gz}, - year = {1997} + AUTHOR = {S. Boutin}, + BOOKTITLE = {TACS'97}, + EDITOR = {Martin Abadi and Takahashi Ito}, + PUBLISHER = SV, + SERIES = lncs, + VOLUME = 1281, + YEAR = {1997} } -@PhdThesis{Bou97These, - author = {S. Boutin}, - title = {R\'eflexions sur les quotients}, - school = {Paris 7}, - year = 1997, - type = {th\`ese d'Universit\'e}, - month = apr +@PHDTHESIS{Bou97These, + AUTHOR = {S. Boutin}, + TITLE = {R\'eflexions sur les quotients}, + SCHOOL = {Paris 7}, + YEAR = 1997, + TYPE = {th\`ese d'Universit\'e}, + MONTH = apr } @ARTICLE{Bru72, @@ -297,6 +296,15 @@ s}, crossref = {Nijmegen93} } +@PHDTHESIS{Cor97, + AUTHOR = {C. Cornes}, + MONTH = nov, + SCHOOL = {{Universit\'e Paris 7}}, + TITLE = {Conception d'un langage de haut niveau de représentation de preuves}, + TYPE = {Th\`ese de Doctorat}, + YEAR = {1997} +} + @MASTERSTHESIS{Cou94a, AUTHOR = {J. Courant}, MONTH = sep, @@ -525,14 +533,23 @@ s}, YEAR = {1994} } -@TechReport{Gim98, - author = {E. Gim\'enez}, - title = {A Tutorial on Recursive Types in Coq}, - institution = {INRIA}, - year = 1998, - month = mar +@TECHREPORT{Gim98, + AUTHOR = {E. Gim\'enez}, + TITLE = {A Tutorial on Recursive Types in Coq}, + INSTITUTION = {INRIA}, + YEAR = 1998, + MONTH = mar } +@UNPUBLISHED{GimCas05, + AUTHOR = {E. Gim\'enez and P. Cast\'eran}, + TITLE = {A Tutorial on [Co-]Inductive Types in Coq}, + INSTITUTION = {INRIA}, + YEAR = 2005, + MONTH = jan, + NOTE = {available at \url{http://coq.inria.fr/doc}} +} + @INPROCEEDINGS{Gimenez95b, AUTHOR = {E. Gim\'enez}, BOOKTITLE = {Workshop on Types for Proofs and Programs}, @@ -607,8 +624,6 @@ s}, YEAR = {1980} } - - @InProceedings{Hue87tapsoft, author = {G. Huet}, title = {Programming of Future Generation Computers}, @@ -630,8 +645,6 @@ s}, YEAR = {1988} } - - @INPROCEEDINGS{Hue88, AUTHOR = {G. Huet}, BOOKTITLE = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, @@ -1115,15 +1128,16 @@ Decomposition}}, note = {\url{http://proofgeneral.inf.ed.ac.uk/}} } +@Book{CoqArt, + title = "Interactive Theorem Proving and Program Development. + Coq'Art: The Calculus of Inductive Constructions", + author = "Yves Bertot and Pierre Castéran", + publisher = "Springer Verlag", + series = "Texts in Theoretical Computer Science. An EATCS series", + year = 2004 + } -@Book{CoqArt, - author = {Yves bertot and Pierre Castéran}, - title = {Coq'Art}, - publisher = {Springer-Verlag}, - year = 2004, - note = {To appear} -} @INCOLLECTION{wadler87, AUTHOR = {P. Wadler}, |