diff options
Diffstat (limited to 'doc/refman/biblio.bib')
| -rw-r--r-- | doc/refman/biblio.bib | 22 |
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 = "{Springer-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 |