aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/biblio.bib
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-09 12:00:10 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-09 12:14:41 +0100
commit9c24cecec3a7381cd924c56ca50c77a49750e2e5 (patch)
tree52eee33926e6791b4d2ac23c04f48404057899b4 /doc/refman/biblio.bib
parent56302f63809494946adf4e805bc61d55ed9d6f14 (diff)
refman: switch all source files to utf8
Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources.
Diffstat (limited to 'doc/refman/biblio.bib')
-rw-r--r--doc/refman/biblio.bib22
1 files changed, 11 insertions, 11 deletions
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index a2895cfcf..fdcc8a7b0 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1,7 +1,7 @@
@String{jfp = "Journal of Functional Programming"}
@String{lncs = "Lecture Notes in Computer Science"}
@String{lnai = "Lecture Notes in Artificial Intelligence"}
-@String{SV = "{Sprin­ger-Verlag}"}
+@String{SV = "{Sprin-ger-Verlag}"}
@InProceedings{Aud91,
author = {Ph. Audebaud},
@@ -310,7 +310,7 @@ s},
author = {C. Cornes},
month = nov,
school = {{Universit\'e Paris 7}},
- title = {Conception d'un langage de haut niveau de représentation de preuves},
+ title = {Conception d'un langage de haut niveau de représentation de preuves},
type = {Th\`ese de Doctorat},
year = {1997}
}
@@ -436,7 +436,7 @@ s},
editor = {G. Huet and G. Plotkin},
pages = {59--79},
publisher = {Cambridge University Press},
- title = {Inductive sets and families in {Martin-Löf's}
+ title = {Inductive sets and families in {Martin-Löf's}
Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory},
volume = {14},
year = {1991}
@@ -456,7 +456,7 @@ s},
author = {J.-C. Filli\^atre},
month = sep,
school = {DEA d'Informatique, ENS Lyon},
- title = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}},
+ title = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}},
year = {1994}
}
@@ -470,7 +470,7 @@ s},
}
@Article{Filliatre03jfp,
- author = {J.-C. Filliâtre},
+ author = {J.-C. Filliâtre},
title = {Verification of Non-Functional Programs
using Interpretations in Type Theory},
journal = jfp,
@@ -488,7 +488,7 @@ s},
@PhDThesis{Filliatre99,
author = {J.-C. Filli\^atre},
title = {Preuve de programmes imp\'eratifs en th\'eorie des types},
- type = {Thèse de Doctorat},
+ type = {Thèse de Doctorat},
school = {Universit\'e Paris-Sud},
year = 1999,
month = {July},
@@ -607,7 +607,7 @@ s},
author = {D. Hirschkoff},
month = sep,
school = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
- title = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
+ title = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
year = {1994}
}
@@ -902,7 +902,7 @@ Intersection Types and Subtyping},
}
@MastersThesis{Mun94,
- author = {C. Muñoz},
+ author = {C. Muñoz},
month = sep,
school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
title = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
@@ -1012,7 +1012,7 @@ the Calculus of Inductive Constructions}},
institution = {INRIA},
month = nov,
number = {1795},
- title = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}},
+ title = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}},
year = {1992}
}
@@ -1075,7 +1075,7 @@ the Calculus of Inductive Constructions}},
@PhDThesis{Bar99,
author = {B. Barras},
school = {Universit\'e Paris 7},
- title = {Auto-validation d'un système de preuves avec familles inductives},
+ title = {Auto-validation d'un système de preuves avec familles inductives},
type = {Th\`ese de Doctorat},
year = {1999}
}
@@ -1177,7 +1177,7 @@ Decomposition}},
@Book{CoqArt,
title = {Interactive Theorem Proving and Program Development.
Coq'Art: The Calculus of Inductive Constructions},
- author = {Yves Bertot and Pierre Castéran},
+ author = {Yves Bertot and Pierre Castéran},
publisher = {Springer Verlag},
series = {Texts in Theoretical Computer Science. An EATCS series},
year = 2004