aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/biblio.bib
diff options
context:
space:
mode:
authorGravatar marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-01 15:40:29 +0000
committerGravatar marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-01 15:40:29 +0000
commit8b827e1540166eed6cdd8f603eb9eb1a5e42ec84 (patch)
treeb09cf6cb624c8cd1ddeaa3d234b795a2ac272214 /doc/biblio.bib
parentbc73bc1ef78f6cb5cabb173e633be9cc96a05180 (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-xdoc/biblio.bib24
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,