aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/faq/fk.bib
diff options
context:
space:
mode:
Diffstat (limited to 'doc/faq/fk.bib')
-rw-r--r--doc/faq/fk.bib126
1 files changed, 63 insertions, 63 deletions
diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib
index d41ab7f09..4d90efcdb 100644
--- a/doc/faq/fk.bib
+++ b/doc/faq/fk.bib
@@ -16,11 +16,11 @@
}
@PHDTHESIS{EGThese,
- author = {Eduardo Giménez},
+ author = {Eduardo Giménez},
title = {Un Calcul de Constructions Infinies et son application
-a la vérification de systèmes communicants},
- type = {thèse d'Université},
- school = {Ecole Normale Supérieure de Lyon},
+a la vérification de systèmes communicants},
+ type = {thèse d'Université},
+ school = {Ecole Normale Supérieure de Lyon},
month = {December},
year = {1996},
}
@@ -29,7 +29,7 @@ a la vérification de systèmes communicants},
%%%%%%% Semantique %%%%%%%
@misc{Sem:cours,
- author = "François Pottier",
+ author = "François Pottier",
title = "{Typage et Programmation}",
year = "2002",
howpublished = "Lecture notes",
@@ -109,7 +109,7 @@ year = {1981}
@book{Coq: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",
@@ -118,8 +118,8 @@ year = {1981}
@phdthesis{Coq:Del01,
AUTHOR = "David Delahaye",
- TITLE = "Conception de langages pour décrire les preuves et les
- automatisations dans les outils d'aide à la preuve",
+ TITLE = "Conception de langages pour décrire les preuves et les
+ automatisations dans les outils d'aide à la preuve",
SCHOOL = {Universit\'e Paris~6},
YEAR = "2001",
Type = {Th\`ese de Doctorat}
@@ -133,7 +133,7 @@ year = {1981}
url = "citeseer.nj.nec.com/gimenez98tutorial.html" }
@phdthesis{Coq:Mun97,
- AUTHOR = "César Mu{\~{n}}oz",
+ AUTHOR = "César Mu{\~{n}}oz",
TITLE = "Un calcul de substitutions pour la repr\'esentation
de preuves partielles en th\'eorie de types",
SCHOOL = {Universit\'e Paris~7},
@@ -191,7 +191,7 @@ year = {1981}
}
@misc{PVS-Tactics:cours,
- author = "César Muñoz",
+ author = "César Muñoz",
title = "Strategies in {PVS}",
howpublished = "Lecture notes",
note = "National Institute of Aerospace",
@@ -288,9 +288,9 @@ year = {1981}
}
@TECHREPORT{modelpa2000,
- AUTHOR = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg
+ AUTHOR = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg
and J.-F. Monin and C. Paulin and A. Petit and D. Rouillard},
- TITLE = {Automates temporisés CALIFE},
+ TITLE = {Automates temporisés CALIFE},
INSTITUTION = {Calife},
YEAR = 2000,
URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F1.1.ps.gz},
@@ -298,8 +298,8 @@ year = {1981}
}
@TECHREPORT{CaFrPaRo2000,
- AUTHOR = {P. Castéran and E. Freund and C. Paulin and D. Rouillard},
- TITLE = {Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions et les p-automates},
+ AUTHOR = {P. Castéran and E. Freund and C. Paulin and D. Rouillard},
+ TITLE = {Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions et les p-automates},
INSTITUTION = {Calife},
YEAR = 2000,
URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F5.4.ps.gz},
@@ -335,7 +335,7 @@ year = {1981}
MONTH = JAN,
SCHOOL = {{Paris 7}},
TITLE = {Extraction de programmes dans le {Calcul des Constructions}},
- TYPE = {Thèse d'université},
+ TYPE = {Thèse d'université},
YEAR = {1989},
URL = {http://www.lri.fr/~paulin/these.ps.gz}
}
@@ -427,11 +427,11 @@ nd Applications},
@PHDTHESIS{Pau96b,
AUTHOR = {Christine Paulin-Mohring},
- TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur},
- SCHOOL = {Université Claude Bernard Lyon I},
+ TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur},
+ SCHOOL = {Université Claude Bernard Lyon I},
YEAR = 1996,
MONTH = DEC,
- TYPE = {Habilitation à diriger les recherches},
+ TYPE = {Habilitation à diriger les recherches},
URL = {http://www.lri.fr/~paulin/habilitation.ps.gz}
}
@@ -488,7 +488,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
}
@TECHREPORT{kmu2002rr,
- AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain},
+ AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain},
TITLE = {Termination of Associative-Commutative Rewriting using Dependency Pairs Criteria},
INSTITUTION = {LRI},
YEAR = 2002,
@@ -509,7 +509,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
}
@INPROCEEDINGS{contejean03wst,
- AUTHOR = {Evelyne Contejean and Claude Marché and Benjamin Monate and Xavier Urbain},
+ AUTHOR = {Evelyne Contejean and Claude Marché and Benjamin Monate and Xavier Urbain},
TITLE = {{Proving Termination of Rewriting with {\sc C\textit{i}ME}}},
CROSSREF = {wst03},
PAGES = {71--73},
@@ -661,7 +661,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
YEAR = {2003},
EDITOR = {Albert Rubio},
MONTH = JUN,
- NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain}
+ NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain}
}
@INPROCEEDINGS{FilliatreLetouzey03,
@@ -740,8 +740,8 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
@INPROCEEDINGS{Filliatre01a,
AUTHOR = {J.-C. Filli\^atre},
- TITLE = {La supériorité de l'ordre supérieur},
- BOOKTITLE = {Journées Francophones des Langages Applicatifs},
+ TITLE = {La supériorité de l'ordre supérieur},
+ BOOKTITLE = {Journées Francophones des Langages Applicatifs},
PAGES = {15--26},
MONTH = {Janvier},
YEAR = 2002,
@@ -749,18 +749,18 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
URL = {http://www.lri.fr/~filliatr/ftp/publis/sos.ps.gz},
CODE = {http://www.lri.fr/~filliatr/ftp/ocaml/misc/koda-ruskey.ps},
ABSTRACT = {
- Nous présentons ici une écriture fonctionnelle de l'algorithme de
+ Nous présentons ici une écriture fonctionnelle de l'algorithme de
Koda-Ruskey, un algorithme pour engendrer une large famille
de codes de Gray. En s'inspirant de techniques de programmation par
- continuation, nous aboutissons à un code de neuf lignes seulement,
- bien plus élégant que les implantations purement impératives
- proposées jusqu'ici, notamment par Knuth. Dans un second temps,
- nous montrons comment notre code peut être légèrement modifié pour
- aboutir à une version de complexité optimale.
- Notre implantation en Objective Caml rivalise d'efficacité avec les
- meilleurs codes C. Nous détaillons les calculs de complexité,
- un exercice intéressant en présence d'ordre supérieur et d'effets de
- bord combinés.}
+ continuation, nous aboutissons à un code de neuf lignes seulement,
+ bien plus élégant que les implantations purement impératives
+ proposées jusqu'ici, notamment par Knuth. Dans un second temps,
+ nous montrons comment notre code peut être légèrement modifié pour
+ aboutir à une version de complexité optimale.
+ Notre implantation en Objective Caml rivalise d'efficacité avec les
+ meilleurs codes C. Nous détaillons les calculs de complexité,
+ un exercice intéressant en présence d'ordre supérieur et d'effets de
+ bord combinés.}
}
@TECHREPORT{Filliatre00c,
@@ -901,33 +901,33 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
YEAR = 1999,
MONTH = {July},
URL = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz},
- ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant
- traits impératifs et fonctionnels dans le cadre de la théorie des
+ ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant
+ traits impératifs et fonctionnels dans le cadre de la théorie des
types.
- La théorie des types constitue un puissant langage de spécification,
- naturellement adapté à la preuve de programmes purement
- fonctionnels. Pour y certifier également des programmes impératifs,
- nous commençons par exprimer leur sémantique de manière purement
+ La théorie des types constitue un puissant langage de spécification,
+ naturellement adapté à la preuve de programmes purement
+ fonctionnels. Pour y certifier également des programmes impératifs,
+ nous commençons par exprimer leur sémantique de manière purement
fonctionnelle. Cette traduction repose sur une analyse statique des
effets de bord des programmes, et sur l'utilisation de la notion de
- monade, notion que nous raffinons en l'associant à la notion d'effet
- de manière générale. Nous montrons que cette traduction est
- sémantiquement correcte.
-
- Puis, à partir d'un programme annoté, nous construisons une preuve
- de sa spécification, traduite de manière fonctionnelle. Cette preuve
- est bâtie sur la traduction fonctionnelle précédemment
- introduite. Elle est presque toujours incomplète, les parties
- manquantes étant autant d'obligations de preuve qui seront laissées
- à la charge de l'utilisateur. Nous montrons que la validité de ces
- obligations entraîne la correction totale du programme.
-
- Nous avons implanté notre travail dans l'assistant de preuve
- Coq, avec lequel il est dès à présent distribué. Cette
- implantation se présente sous la forme d'une tactique prenant en
- argument un programme annoté et engendrant les obligations de
- preuve. Plusieurs algorithmes non triviaux ont été certifiés à
+ monade, notion que nous raffinons en l'associant à la notion d'effet
+ de manière générale. Nous montrons que cette traduction est
+ sémantiquement correcte.
+
+ Puis, à partir d'un programme annoté, nous construisons une preuve
+ de sa spécification, traduite de manière fonctionnelle. Cette preuve
+ est bâtie sur la traduction fonctionnelle précédemment
+ introduite. Elle est presque toujours incomplète, les parties
+ manquantes étant autant d'obligations de preuve qui seront laissées
+ à la charge de l'utilisateur. Nous montrons que la validité de ces
+ obligations entraîne la correction totale du programme.
+
+ Nous avons implanté notre travail dans l'assistant de preuve
+ Coq, avec lequel il est dès à présent distribué. Cette
+ implantation se présente sous la forme d'une tactique prenant en
+ argument un programme annoté et engendrant les obligations de
+ preuve. Plusieurs algorithmes non triviaux ont été certifiés à
l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de
Knuth-Morris-Pratt).}
}
@@ -1081,7 +1081,7 @@ tique},
}
@InCollection{cc,
- author = {Thierry Coquand and Gérard Huet},
+ author = {Thierry Coquand and Gérard Huet},
title = {The Calculus of Constructions},
booktitle = {Information and Computation},
year = {1988},
@@ -1095,7 +1095,7 @@ tique},
title = {Inductively defined types},
booktitle = {Proceedings of Colog'88},
year = {1990},
- editor = {P. Martin-Löf and G. Mints},
+ editor = {P. Martin-Löf and G. Mints},
volume = {417},
series = {LNCS},
publisher = {Springer-Verlag}
@@ -1318,7 +1318,7 @@ s},
}
@INPROCEEDINGS{CoHu85a,
- AUTHOR = {Thierry Coquand and Gérard Huet},
+ AUTHOR = {Thierry Coquand and Gérard Huet},
ADDRESS = {Linz},
BOOKTITLE = {EUROCAL'85},
PUBLISHER = SV,
@@ -1329,7 +1329,7 @@ s},
}
@INPROCEEDINGS{CoHu85b,
- AUTHOR = {Thierry Coquand and Gérard Huet},
+ AUTHOR = {Thierry Coquand and Gérard Huet},
BOOKTITLE = {Logic Colloquium'85},
EDITOR = {The Paris Logic Group},
PUBLISHER = {North-Holland},
@@ -1338,7 +1338,7 @@ s},
}
@ARTICLE{CoHu86,
- AUTHOR = {Thierry Coquand and Gérard Huet},
+ AUTHOR = {Thierry Coquand and Gérard Huet},
JOURNAL = {Information and Computation},
NUMBER = {2/3},
TITLE = {The {Calculus of Constructions}},
@@ -2092,7 +2092,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}
}
@@ -2177,7 +2177,7 @@ Decomposition}},
@Book{CoqArt,
- author = {Yves bertot and Pierre Castéran},
+ author = {Yves bertot and Pierre Castéran},
title = {Coq'Art},
publisher = {Springer-Verlag},
year = 2004,
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 12:46:21 +0000