diff options
author | marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-01 15:40:29 +0000 |
---|---|---|
committer | marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-01 15:40:29 +0000 |
commit | 8b827e1540166eed6cdd8f603eb9eb1a5e42ec84 (patch) | |
tree | b09cf6cb624c8cd1ddeaa3d234b795a2ac272214 /doc/biblio.bib | |
parent | bc73bc1ef78f6cb5cabb173e633be9cc96a05180 (diff) |
version et style
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8371 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/biblio.bib')
-rwxr-xr-x | doc/biblio.bib | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/doc/biblio.bib b/doc/biblio.bib index 06ef069d2..3e1d96344 100755 --- a/doc/biblio.bib +++ b/doc/biblio.bib @@ -120,10 +120,10 @@ s}, @PhdThesis{Bou97These, author = {S. Boutin}, - title = {Réflexions sur les quotients}, + title = {R\'eflexions sur les quotients}, school = {Paris 7}, year = 1997, - type = {thèse d'Université}, + type = {th\`ese d'Universit\'e}, month = apr } @@ -166,7 +166,7 @@ s}, @PHDTHESIS{CPar95, AUTHOR = {C. Parent}, - SCHOOL = {Ecole {Normale} {Supérieure} de {Lyon}}, + SCHOOL = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, TITLE = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}}, YEAR = {1995} } @@ -179,7 +179,7 @@ s}, } @INPROCEEDINGS{ChiPotSimp03, - AUTHOR = {Laurent Chicli and Loïc Pottier and Carlos Simpson}, + AUTHOR = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson}, ADDRESS = {Berg en Dal, The Netherlands}, TITLE = {Mathematical Quotients and Quotient Types in Coq}, BOOKTITLE = {TYPES'02}, @@ -229,7 +229,7 @@ s}, @INPROCEEDINGS{CoPa89, AUTHOR = {Th. Coquand and C. Paulin-Mohring}, BOOKTITLE = {Proceedings of Colog'88}, - EDITOR = {P. Martin-Löf and G. Mints}, + EDITOR = {P. Martin-L\"of and G. Mints}, PUBLISHER = {Springer-Verlag}, SERIES = {LNCS}, TITLE = {Inductively defined types}, @@ -299,15 +299,15 @@ s}, AUTHOR = {J. Courant}, MONTH = sep, SCHOOL = {DEA d'Informatique, ENS Lyon}, - TITLE = {Explicitation de preuves par récurrence implicite}, + TITLE = {Explicitation de preuves par r\'ecurrence implicite}, YEAR = {1994} } @INPROCEEDINGS{Del99, author = "Delahaye, D.", - title = "Information {R}etrieval in a {{\sf Coq}} {P}roof {L}ibrary using - {T}ype {I}somorphisms", - booktitle = "Proceedings of TYPES'99, Lökeberg", + title = "Information Retrieval in a Coq Proof Library using + Type Isomorphisms", + booktitle = {Proceedings of TYPES'99, L\"okeberg}, publisher = "Springer-Verlag LNCS", year = "1999", url = @@ -332,9 +332,9 @@ s}, @INPROCEEDINGS{DelMay01, author = "Delahaye, D. and Mayero, M.", - title = "{\tt Field}: une procédure de décision pour les nombres réels + title = "{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels en {{\sf Coq}}", - booktitle = "Journées Francophones des Langages Applicatifs, Pontarlier", + booktitle = "Journ\'ees Francophones des Langages Applicatifs, Pontarlier", publisher = "INRIA", month = "Janvier", year = "2001", @@ -511,7 +511,7 @@ s}, } @TechReport{Gim98, - author = {E. Giménez}, + author = {E. Gim\'enez}, title = {A Tutorial on Recursive Types in Coq}, institution = {INRIA}, year = 1998, |