maj biblio faq

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8496 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 819 insertions, 0 deletions

diff --git a/doc/newfaq/fk.bib b/doc/newfaq/fk.bib
index 58f111947d..576e1ccfe1 100644
--- a/doc/newfaq/fk.bib
+++ b/doc/newfaq/fk.bib
@@ -286,3 +286,822 @@ year = {1981}
   year = 1999,
 }
 
+@INPROCEEDINGS{CoPa89,
+  AUTHOR = {Th. Coquand and C. Paulin-Mohring},
+  BOOKTITLE = {Proceedings of Colog'88},
+  EDITOR = {P. Martin-L{\"o}f and G. Mints},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 417,
+  PUBLISHER = {Springer-Verlag},
+  TITLE = {Inductively defined types},
+  YEAR = {1990}
+}
+
+@MANUAL{CoqManualV7,
+  AUTHOR = {{The {Coq} Development Team}},
+  TITLE = {{The Coq Proof Assistant Reference Manual -- Version
+ V7.1}},
+  YEAR = {2001},
+  MONTH = OCT,
+  NOTE = {http://coq.inria.fr}
+}
+
+@MANUAL{CoqManual96,
+  TITLE = {The {Coq Proof Assistant Reference Manual} Version 6.1},
+  AUTHOR = {B. Barras and S. Boutin and C. Cornes and J. Courant and 
+                  J.-C. Filli\^atre and 
+                  H. Herbelin and G. Huet and P. Manoury and C. Mu{\~{n}}oz and
+                  C. Murthy and C. Parent and C. Paulin-Mohring and
+                  A. Sa{\"\i}bi and B. Werner},
+  ORGANIZATION = {{INRIA-Rocquencourt}-{CNRS-ENS Lyon}},
+  URL = {ftp://ftp.inria.fr/INRIA/coq/V6.1/doc/Reference-Manual.dvi.gz},
+  YEAR = 1996,
+  MONTH = DEC
+}
+
+@MANUAL{CoqTutorial99,
+  AUTHOR = {G.~Huet and G.~Kahn and Ch.~Paulin-Mohring},
+  TITLE = {The {\sf Coq} Proof Assistant - A tutorial - Version 6.3},
+  MONTH = JUL,
+  YEAR = {1999},
+  ABSTRACT = {http://coq.inria.fr/doc/tutorial.html}
+}
+
+@MANUAL{CoqTutorialV7,
+  AUTHOR = {G.~Huet and G.~Kahn and Ch.~Paulin-Mohring},
+  TITLE = {The {\sf Coq} Proof Assistant - A tutorial - Version 7.1},
+  MONTH = OCT,
+  YEAR = {2001},
+  NOTE = {http://coq.inria.fr}
+}
+
+@TECHREPORT{modelpa2000,
+  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},
+  INSTITUTION = {Calife},
+  YEAR = 2000,
+  URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F1.1.ps.gz},
+  TYPE = {Fourniture {F1.1}}
+}
+
+@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},
+  INSTITUTION = {Calife},
+  YEAR = 2000,
+  URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F5.4.ps.gz},
+  TYPE = {Fourniture {F5.4}}
+}
+
+@PROCEEDINGS{TPHOLs99,
+  TITLE = {International Conference on 
+                  Theorem Proving in Higher Order Logics (TPHOLs'99)},
+  YEAR = 1999,
+  EDITOR = {Y. Bertot and G. Dowek and C. Paulin-Mohring and L. Th{\'e}ry},
+  SERIES = {Lecture Notes in Computer Science},
+  MONTH = SEP,
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  ADDRESS = {Nice},
+  TYPE_PUBLI = {editeur}
+}
+
+@INPROCEEDINGS{Pau01,
+  AUTHOR = {Christine Paulin-Mohring},
+  TITLE = {Modelisation of Timed Automata in {Coq}},
+  BOOKTITLE = {Theoretical Aspects of Computer Software (TACS'2001)},
+  PAGES = {298--315},
+  YEAR = 2001,
+  EDITOR = {N. Kobayashi and B. Pierce},
+  VOLUME = 2215,
+  SERIES = {Lecture Notes in Computer Science},
+  PUBLISHER = {Springer-Verlag}
+}
+
+@PHDTHESIS{Moh89b,
+  AUTHOR = {C. Paulin-Mohring},
+  MONTH = JAN,
+  SCHOOL = {{Paris 7}},
+  TITLE = {Extraction de programmes dans le {Calcul des Constructions}},
+  TYPE = {Thèse d'université},
+  YEAR = {1989},
+  URL = {http://www.lri.fr/~paulin/these.ps.gz}
+}
+
+@ARTICLE{HuMo92,
+  AUTHOR = {G. Huet and C. Paulin-Mohring},
+  EDITION = {INRIA},
+  JOURNAL = {Courrier du CNRS - Informatique},
+  TITLE = {Preuves et Construction de Programmes},
+  YEAR = {1992},
+  CATEGORY = {national}
+}
+
+@INPROCEEDINGS{LePa94,
+  AUTHOR = {F. Leclerc and C. Paulin-Mohring},
+  TITLE = {Programming with Streams in {Coq}. A case study : The Sieve of Eratosthenes},
+  EDITOR = {H. Barendregt and T. Nipkow},
+  VOLUME = 806,
+  SERIES = {Lecture Notes in Computer Science},
+  BOOKTITLE = {{Types for Proofs and Programs, Types' 93}},
+  YEAR = 1994,
+  PUBLISHER = {Springer-Verlag}
+}
+
+@INPROCEEDINGS{Moh86,
+  AUTHOR = {C. Mohring},
+  ADDRESS = {Cambridge, MA},
+  BOOKTITLE = {Symposium on Logic in Computer Science},
+  PUBLISHER = {IEEE Computer Society Press},
+  TITLE = {Algorithm Development in the {Calculus of Constructions}},
+  YEAR = {1986}
+}
+
+@INPROCEEDINGS{Moh89a,
+  AUTHOR = {C. Paulin-Mohring},
+  ADDRESS = {Austin},
+  BOOKTITLE = {Sixteenth Annual ACM Symposium on Principles of Programming Languages},
+  MONTH = JAN,
+  PUBLISHER = {ACM},
+  TITLE = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}},
+  YEAR = {1989}
+}
+
+@INCOLLECTION{Moh89c,
+  AUTHOR = {C. Paulin-Mohring},
+  TITLE = {{R\'ealisabilit\'e et extraction de programmes}},
+  BOOKTITLE = {Logique et Informatique : une introduction},
+  PUBLISHER = {INRIA},
+  YEAR = 1991,
+  EDITOR = {B. Courcelle},
+  VOLUME = 8,
+  SERIES = {Collection Didactique},
+  PAGES = {163-180},
+  CATEGORY = {national}
+}
+
+@INPROCEEDINGS{Moh93,
+  AUTHOR = {C. Paulin-Mohring},
+  BOOKTITLE = {Proceedings of the conference Typed Lambda Calculi a
+nd Applications},
+  EDITOR = {M. Bezem and J.-F. Groote},
+  INSTITUTION = {LIP-ENS Lyon},
+  NOTE = {LIP research report 92-49},
+  NUMBER = 664,
+  SERIES = {Lecture Notes in Computer Science},
+  TITLE = {{Inductive Definitions in the System {Coq} - Rules and Properties}},
+  TYPE = {research report},
+  YEAR = 1993
+}
+
+@ARTICLE{PaWe92,
+  AUTHOR = {C. Paulin-Mohring and B. Werner},
+  JOURNAL = {Journal of Symbolic Computation},
+  TITLE = {{Synthesis of ML programs in the system Coq}},
+  VOLUME = {15},
+  YEAR = {1993},
+  PAGES = {607--640}
+}
+
+@INPROCEEDINGS{Pau96,
+  AUTHOR = {C. Paulin-Mohring},
+  TITLE = {Circuits as streams in {Coq} : Verification of a sequential multiplier},
+  BOOKTITLE = {Types for Proofs and Programs, TYPES'95},
+  EDITOR = {S. Berardi and M. Coppo},
+  SERIES = {Lecture Notes in Computer Science},
+  YEAR = 1996,
+  VOLUME = 1158
+}
+
+@PHDTHESIS{Pau96b,
+  AUTHOR = {C. Paulin-Mohring},
+  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},
+  URL = {http://www.lri.fr/~paulin/habilitation.ps.gz}
+}
+
+@INPROCEEDINGS{PfPa89,
+  AUTHOR = {F. Pfenning and C. Paulin-Mohring},
+  BOOKTITLE = {Proceedings of Mathematical Foundations of Programming Semantics},
+  NOTE = {technical report CMU-CS-89-209},
+  PUBLISHER = {Springer-Verlag},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 442,
+  TITLE = {Inductively defined types in the {Calculus of Constructions}},
+  YEAR = {1990}
+}
+
+@MISC{krakatoa02,
+  AUTHOR = {Claude March\'e and Christine Paulin and Xavier Urbain},
+  TITLE = {The \textsc{Krakatoa} proof tool},
+  YEAR = 2002,
+  NOTE = {\url{http://krakatoa.lri.fr/}}
+}
+
+@ARTICLE{marche03jlap,
+  AUTHOR = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain},
+  TITLE = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}},
+  JOURNAL = {Journal of Logic and Algebraic Programming},
+  YEAR = 2003,
+  NOTE = {To appear},
+  URL = {http://krakatoa.lri.fr},
+  TOPICS = {team}
+}
+@ARTICLE{marche04jlap,
+  AUTHOR = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain},
+  TITLE = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}},
+  JOURNAL = {Journal of Logic and Algebraic Programming},
+  YEAR = 2004,
+  VOLUME = 58,
+  NUMBER = {1--2},
+  PAGES = {89--106},
+  URL = {http://krakatoa.lri.fr},
+  TOPICS = {team}
+}
+
+@TECHREPORT{catano03deliv,
+  AUTHOR = {N{\'e}stor Cata{\~n}o and Marek Gawkowski and
+Marieke Huisman and Bart Jacobs and Claude March{\'e} and Christine Paulin
+and Erik Poll and Nicole Rauch and Xavier Urbain},
+  TITLE = {Logical Techniques for Applet Verification},
+  INSTITUTION = {VerifiCard Project},
+  YEAR = 2003,
+  TYPE = {Deliverable},
+  NUMBER = {5.2},
+  TOPICS = {team},
+  NOTE = {Available from \url{http://www.verificard.org}}
+}
+
+@TECHREPORT{kmu2002rr,
+  AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain},
+  TITLE = {Termination of Associative-Commutative Rewriting using Dependency Pairs Criteria},
+  INSTITUTION = {LRI},
+  YEAR = 2002,
+  TYPE = {Research Report},
+  NUMBER = 1304,
+  TYPE_PUBLI = {interne},
+  TOPICS = {team},
+  NOTE = {\url{http://www.lri.fr/~urbain/textes/rr1304.ps.gz}},
+  URL = {http://www.lri.fr/~urbain/textes/rr1304.ps.gz}
+}
+
+@ARTICLE{marche2004jsc,
+  AUTHOR = {Claude March\'e and Xavier Urbain},
+  TITLE = {Modular {\&} Incremental Proofs of {AC}-Termination},
+  JOURNAL = {Journal of Symbolic Computation},
+  YEAR = 2004,
+  TOPICS = {team}
+}
+
+@INPROCEEDINGS{contejean03wst,
+  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},
+  NOTE = {\url{http://cime.lri.fr/}},
+  URL = {http://cime.lri.fr/},
+  YEAR = 2003,
+  TYPE_PUBLI = {icolcomlec},
+  TOPICS = {team}
+}
+
+@TECHREPORT{contejean04rr,
+  AUTHOR = {Evelyne Contejean and Claude March{\'e} and Ana-Paula Tom{\'a}s and Xavier Urbain},
+  TITLE = {Mechanically proving termination using polynomial interpretations},
+  INSTITUTION = {LRI},
+  YEAR = {2004},
+  TYPE = {Research Report},
+  NUMBER = {1382},
+  TYPE_PUBLI = {interne},
+  TOPICS = {team},
+  URL = {http://www.lri.fr/~urbain/textes/rr1382.ps.gz}
+}
+
+@UNPUBLISHED{duran_sub,
+  AUTHOR = {Francisco Duran and Salvador Lucas and
+  Claude {March\'e} and {Jos\'e} Meseguer and Xavier Urbain},
+  TITLE = {Termination of Membership Equational Programs},
+  NOTE = {Submitted}
+}
+
+@PROCEEDINGS{comon95lncs,
+  TITLE = {Term Rewriting},
+  BOOKTITLE = {Term Rewriting},
+  TOPICS = {team, cclserver},
+  YEAR = 1995,
+  EDITOR = {Hubert Comon and Jean-Pierre Jouannaud},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = {909},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  ORGANIZATION = {French Spring School of Theoretical Computer
+		  Science},
+  TYPE_PUBLI = {editeur},
+  CLEF_LABO = {CJ95}
+}
+
+@PROCEEDINGS{lics94,
+  TITLE = {Proceedings of the Ninth Annual IEEE Symposium on Logic
+			in Computer Science},
+  BOOKTITLE = {Proceedings of the Ninth Annual IEEE Symposium on Logic
+			in Computer Science},
+  YEAR = 1994,
+  MONTH = JUL,
+  ADDRESS = {Paris, France},
+  ORGANIZATION = {{IEEE} Comp. Soc. Press}
+}
+
+@PROCEEDINGS{rta91,
+  TITLE = {4th International Conference on Rewriting Techniques and
+                        Applications},
+  BOOKTITLE = {4th International Conference on Rewriting Techniques and
+                        Applications},
+  EDITOR = {Ronald. V. Book},
+  YEAR = 1991,
+  MONTH = APR,
+  ADDRESS = {Como, Italy},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 488
+}
+
+@PROCEEDINGS{rta96,
+  TITLE = {7th International Conference on Rewriting Techniques and
+			Applications},
+  BOOKTITLE = {7th International Conference on Rewriting Techniques and
+			Applications},
+  EDITOR = {Harald Ganzinger},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  YEAR = 1996,
+  MONTH = JUL,
+  ADDRESS = {New Brunswick, NJ, USA},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 1103
+}
+
+@PROCEEDINGS{rta97,
+  TITLE = {8th International Conference on Rewriting Techniques and
+			Applications},
+  BOOKTITLE = {8th International Conference on Rewriting Techniques and
+			Applications},
+  EDITOR = {Hubert Comon},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  YEAR = 1997,
+  MONTH = JUN,
+  ADDRESS = {Barcelona, Spain},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = {1232}
+}
+
+@PROCEEDINGS{rta98,
+  TITLE = {9th International Conference on Rewriting Techniques and
+			Applications},
+  BOOKTITLE = {9th International Conference on Rewriting Techniques and
+			Applications},
+  EDITOR = {Tobias Nipkow},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  YEAR = 1998,
+  MONTH = APR,
+  ADDRESS = {Tsukuba, Japan},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = {1379}
+}
+
+@PROCEEDINGS{rta00,
+  TITLE = {11th International Conference on Rewriting Techniques and Applications},
+  BOOKTITLE = {11th International Conference on Rewriting Techniques and Applications},
+  EDITOR = {Leo Bachmair},
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 1833,
+  MONTH = JUL,
+  YEAR = 2000,
+  ADDRESS = {Norwich, UK}
+}
+
+@PROCEEDINGS{srt95,
+  TITLE = {Proceedings of the Conference on Symbolic Rewriting
+		  Techniques},
+  BOOKTITLE = {Proceedings of the Conference on Symbolic Rewriting
+		  Techniques},
+  YEAR = 1995,
+  EDITOR = {Manuel Bronstein and Volker Weispfenning},
+  ADDRESS = {Monte Verita, Switzerland}
+}
+
+@BOOK{comon01cclbook,
+  BOOKTITLE = {Constraints in Computational Logics},
+  TITLE = {Constraints in Computational Logics},
+  EDITOR = {Hubert Comon and Claude March{\'e} and Ralf Treinen},
+  YEAR = 2001,
+  PUBLISHER = {{Sprin\-ger-Verlag}},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 2002,
+  TOPICS = {team},
+  TYPE_PUBLI = {editeur}
+}
+
+@PROCEEDINGS{wst03,
+  BOOKTITLE = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}},
+  TITLE = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}},
+  YEAR = {2003},
+  EDITOR = {Albert Rubio},
+  MONTH = JUN,
+  NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain}
+
+@INPROCEEDINGS{FilliatreLetouzey03,
+  AUTHOR = {J.-C. Filli\^atre and P. Letouzey},
+  TITLE = {{Functors for Proofs and Programs}},
+  BOOKTITLE = {Proceedings of The European Symposium on Programming},
+  YEAR = 2004,
+  ADDRESS = {Barcelona, Spain},
+  MONTH = {March 29-April 2},
+  NOTE = {To appear},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz}
+}
+
+@TECHREPORT{Filliatre03,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Why: a multi-language multi-prover verification tool}},
+  INSTITUTION = {{LRI, Universit\'e Paris Sud}},
+  TYPE = {{Research Report}},
+  NUMBER = {1366},
+  MONTH = {March},
+  YEAR = 2003,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}
+}
+
+@ARTICLE{FilliatrePottier02,
+  AUTHOR = {J.-C. Filli{\^a}tre and F. Pottier},
+  TITLE = {{Producing All Ideals of a Forest, Functionally}},
+  JOURNAL = {Journal of Functional Programming},
+  VOLUME = 13,
+  NUMBER = 5,
+  PAGES = {945--956},
+  MONTH = {September},
+  YEAR = 2003,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/kr-fp.ps.gz},
+  ABSTRACT = {
+  We present a functional implementation of Koda and Ruskey's
+  algorithm for generating all ideals of a forest poset as a Gray
+  code. Using a continuation-based approach, we give an extremely
+  concise formulation of the algorithm's core. Then, in a number of
+  steps, we derive a first-order version whose efficiency is
+  comparable to a C implementation given by Knuth.}
+}
+
+@UNPUBLISHED{FORS01,
+  AUTHOR = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar},
+  TITLE = {Deciding Propositional Combinations of Equalities and Inequalities},
+  NOTE = {Unpublished},
+  MONTH = OCT,
+  YEAR = 2001,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/ics.ps},
+  ABSTRACT = { 
+  We address the problem of combining individual decision procedures
+  into a single decision procedure.  Our combination approach is based
+  on using the canonizer obtained from Shostak's combination algorithm
+  for equality.  We illustrate our approach with a combination
+  algorithm for equality, disequality, arithmetic inequality, and
+  propositional logic.  Unlike the Nelson--Oppen combination where the
+  processing of equalities is distributed across different closed
+  decision procedures, our combination involves the centralized
+  processing of equalities in a single procedure.  The termination
+  argument for the combination is based on that for Shostak's
+  algorithm.  We also give soundness and completeness arguments.}
+}
+
+@INPROCEEDINGS{ICS,
+  AUTHOR = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar},
+  TITLE = {{ICS: Integrated Canonization and Solving (Tool presentation)}},
+  BOOKTITLE = {Proceedings of CAV'2001},
+  EDITOR = {G. Berry and H. Comon and A. Finkel},
+  PUBLISHER = {Springer-Verlag},
+  SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 2102,
+  PAGES = {246--249},
+  YEAR = 2001
+}
+
+@INPROCEEDINGS{Filliatre01a,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {La supériorité de l'ordre supérieur},
+  BOOKTITLE = {Journées Francophones des Langages Applicatifs},
+  PAGES = {15--26},
+  MONTH = {Janvier},
+  YEAR = 2002,
+  ADDRESS = {Anglet, France},
+  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
+  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.}
+}
+
+@TECHREPORT{Filliatre00c,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Design of a proof assistant: Coq version 7}},
+  INSTITUTION = {{LRI, Universit\'e Paris Sud}},
+  TYPE = {{Research Report}},
+  NUMBER = {1369},
+  MONTH = {October},
+  YEAR = 2000,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/coqv7.ps.gz},
+  ABSTRACT = {
+  We present the design and implementation of the new version of the
+  Coq proof assistant. The main novelty is the isolation of the
+  critical part of the system, which consists in a type checker for
+  the Calculus of Inductive Constructions. This kernel is now
+  completely independent of the rest of the system and has been
+  rewritten in a purely functional way. This leads to greater clarity
+  and safety, without compromising efficiency. It also opens the way to
+  the ``bootstrap'' of the Coq system, where the kernel will be
+  certified using Coq itself.}
+}
+
+@TECHREPORT{Filliatre00b,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Hash consing in an ML framework}},
+  INSTITUTION = {{LRI, Universit\'e Paris Sud}},
+  TYPE = {{Research Report}},
+  NUMBER = {1368},
+  MONTH = {September},
+  YEAR = 2000,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing.ps.gz},
+  ABSTRACT = {
+  Hash consing is a technique to share values that are structurally
+  equal. Beyond the obvious advantage of saving memory blocks, hash
+  consing may also be used to gain speed in several operations (like
+  equality test) and data structures (like sets or maps) when sharing is
+  maximal. However, physical adresses cannot be used directly for this
+  purpose when the garbage collector is likely to move blocks
+  underneath. We present an easy solution in such a framework, with
+  many practical benefits.}
+}
+
+@MISC{ocamlweb,
+  AUTHOR = {J.-C. Filli\^atre and C. March\'e},
+  TITLE = {{ocamlweb, a literate programming tool for Objective Caml}},
+  NOTE = {Available at \url{http://www.lri.fr/~filliatr/ocamlweb/}},
+  URL = {http://www.lri.fr/~filliatr/ocamlweb/}
+}
+
+@ARTICLE{Filliatre00a,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Verification of Non-Functional Programs 
+                   using Interpretations in Type Theory}},
+  JOURNAL = {Journal of Functional Programming},
+  VOLUME = 13,
+  NUMBER = 4,
+  PAGES = {709--745},
+  MONTH = {July},
+  YEAR = 2003,
+  NOTE = {English translation of~\cite{Filliatre99}.},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz},
+  ABSTRACT = {We study the problem of certifying programs combining imperative and
+  functional features within the general framework of type theory.
+  
+  Type theory constitutes a powerful specification language, which is
+  naturally suited for the proof of purely functional programs. To
+  deal with imperative programs, we propose a logical interpretation
+  of an annotated program as a partial proof of its specification. The
+  construction of the corresponding partial proof term is based on a
+  static analysis of the effects of the program, and on the use of
+  monads. The usual notion of monads is refined in order to account
+  for the notion of effect. The missing subterms in the partial proof
+  term are seen as proof obligations, whose actual proofs are left to
+  the user. We show that the validity of those proof obligations
+  implies the total correctness of the program.
+  We also establish a result of partial completeness.
+  
+  This work has been implemented in the Coq proof assistant.
+  It appears as a tactic taking an annotated program as argument and
+  generating a set of proof obligations. Several nontrivial
+  algorithms have been certified using this tactic.}
+}
+
+@ARTICLE{Filliatre99c,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Formal Proof of a Program: Find}},
+  JOURNAL = {Science of Computer Programming},
+  YEAR = 2001,
+  NOTE = {To appear},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz},
+  ABSTRACT = {In 1971, C.~A.~R.~Hoare gave the proof of correctness and termination of a
+  rather complex algorithm, in a paper entitled \emph{Proof of a
+    program: Find}. It is a hand-made proof, where the
+  program is given together with its formal specification and where
+  each step is fully 
+  justified by a mathematical reasoning.  We present here a formal
+  proof of the same program in the system Coq, using the
+  recent tactic of the system developed to establishing the total
+  correctness of 
+  imperative programs. We follow Hoare's paper as close as
+  possible, keeping the same program and the same specification. We
+  show that we get exactly the same proof obligations, which are
+  proved in a straightforward way, following the original paper.
+  We also explain how more informal reasonings of Hoare's proof are
+  formalized in the system Coq.
+  This demonstrates the adequacy of the system Coq in the
+  process of certifying imperative programs.}
+}
+
+@TECHREPORT{Filliatre99b,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{A theory of monads parameterized by effects}},
+  INSTITUTION = {{LRI, Universit\'e Paris Sud}},
+  TYPE = {{Research Report}},
+  NUMBER = {1367},
+  MONTH = {November},
+  YEAR = 1999,
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/monads.ps.gz},
+  ABSTRACT = {Monads were introduced in computer science to express the semantics
+  of programs with computational effects, while type and effect
+  inference was introduced to mark out those effects.
+  In this article, we propose a combination of the notions of effects
+  and monads, where the monadic operators are parameterized by effects.
+  We establish some relationships between those generalized monads and
+  the classical ones.
+  Then we use a generalized monad to translate imperative programs
+  into purely functional ones. We establish the correctness of that
+  translation. This work has been put into practice in the Coq proof
+  assistant to establish the correctness of imperative programs.}
+}
+
+@PHDTHESIS{Filliatre99,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
+  TYPE = {Th{\`e}se de Doctorat},
+  SCHOOL = {Universit\'e Paris-Sud},
+  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
+  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
+  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 à
+  l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de
+  Knuth-Morris-Pratt).}
+}
+
+@INPROCEEDINGS{FilliatreMagaud99,
+  AUTHOR = {J.-C. Filli\^atre and N. Magaud},
+  TITLE = {{Certification of sorting algorithms in the system Coq}},
+  BOOKTITLE = {Theorem Proving in Higher Order Logics: 
+                  Emerging Trends},
+  YEAR = 1999,
+  ABSTRACT = {We present the formal proofs of total correctness of three sorting
+  algorithms in the system Coq, namely \textit{insertion sort},
+  \textit{quicksort} and \textit{heapsort}. The implementations are
+  imperative programs working in-place on a given array. Those
+  developments demonstrate the usefulness of inductive types and higher-order
+  logic in the process of software certification. They also
+  show that the proof of rather complex algorithms may be done in a
+  small amount of time --- only a few days for each development ---
+  and without great difficulty.},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}
+}
+
+@INPROCEEDINGS{Filliatre98,
+  AUTHOR = {J.-C. Filli\^atre},
+  TITLE = {{Proof of Imperative Programs in Type Theory}},
+  BOOKTITLE = {International Workshop, TYPES '98, Kloster Irsee, Germany},
+  PUBLISHER = {Springer-Verlag},
+  VOLUME = 1657,
+  SERIES = {Lecture Notes in Computer Science},
+  MONTH = MAR,
+  YEAR = {1998},
+  ABSTRACT = {We present a new approach to certifying imperative programs,
+  in the context of Type Theory.
+  The key is a functional translation of imperative programs, which is
+  made possible by an analysis of their effects.
+  On sequential imperative programs, we get the same proof
+  obligations as those given by Floyd-Hoare logic,
+  but our approach also includes functional constructions.
+  As a side-effect, we propose a way to eradicate the use of auxiliary
+  variables in specifications.
+  This work has been implemented in the Coq Proof Assistant and applied
+  on non-trivial examples.},
+  URL = {http://www.lri.fr/~filliatr/ftp/publis/types98.ps.gz}
+}
+
+@TECHREPORT{Filliatre97,
+  AUTHOR = {J.-C. Filli\^atre},
+  INSTITUTION = {LIP - ENS Lyon},
+  NUMBER = {97--04},
+  TITLE = {{Finite Automata Theory in Coq: 
+                              A constructive proof of Kleene's theorem}},
+  TYPE = {Research Report},
+  MONTH = {February},
+  YEAR = {1997},
+  ABSTRACT = {We describe here a development in the system Coq
+  of a piece of Finite Automata Theory. The main result is the Kleene's
+  theorem, expressing that regular expressions and finite automata
+  define the same languages. From a constructive proof of this result,
+  we automatically obtain a functional program that compiles any
+  regular expression into a finite automata, which constitutes the main
+  part of the implementation of {\tt grep}-like programs. This
+  functional program is obtained by the automatic method of {\em
+  extraction} which removes the logical parts of the proof to keep only
+  its informative contents.  Starting with an idea of what we would
+  have written in ML, we write the specification and do the proofs in
+  such a way that we obtain the expected program, which is therefore
+  efficient.},
+  URL = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR97/RR97-04.ps.Z}
+}
+
+@TECHREPORT{Filliatre95,
+  AUTHOR = {J.-C. Filli\^atre},
+  INSTITUTION = {LIP - ENS Lyon},
+  NUMBER = {96--25},
+  TITLE = {{A decision procedure for Direct Predicate
+                              Calculus: study and implementation in
+                              the Coq system}},
+  TYPE = {Research Report},
+  MONTH = {February},
+  YEAR = {1995},
+  ABSTRACT = {The paper of J. Ketonen and R. Weyhrauch \emph{A
+  decidable fragment of Predicate Calculus} defines a decidable
+  fragment of first-order predicate logic - Direct Predicate Calculus
+  - as the subset which is provable in Gentzen sequent calculus
+  without the contraction rule, and gives an effective decision
+  procedure for it. This report is a detailed study of this
+  procedure. We extend the decidability to non-prenex formulas. We
+  prove that the intuitionnistic fragment is still decidable, with a
+  refinement of the same procedure. An intuitionnistic version has
+  been implemented in the Coq system using a translation into
+  natural deduction.},
+  URL = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR96/RR96-25.ps.Z}
+}
+
+@TECHREPORT{Filliatre94,
+  AUTHOR = {J.-C. Filli\^atre},
+  MONTH = {Juillet},
+  INSTITUTION = {Ecole Normale Sup\'erieure},
+  TITLE = {{Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct~: \'etude et impl\'ementation dans le syst\`eme Coq}},
+  TYPE = {Rapport de {DEA}},
+  YEAR = {1994},
+  URL = {ftp://ftp.lri.fr/LRI/articles/filliatr/memoire.dvi.gz}
+}
+
+@TECHREPORT{CourantFilliatre93,
+  AUTHOR = {J. Courant et J.-C. Filli\^atre},
+  MONTH = {Septembre},
+  INSTITUTION = {Ecole Normale Sup\'erieure},
+  TITLE = {{Formalisation de la th\'eorie des langages 
+                              formels en Coq}},
+  TYPE = {Rapport de ma\^{\i}trise},
+  YEAR = {1993},
+  URL = {http://www.ens-lyon.fr/~jcourant/stage_maitrise.dvi.gz},
+  URL2 = {http://www.ens-lyon.fr/~jcourant/stage_maitrise.ps.gz}
+}
+
+@INPROCEEDINGS{tphols2000-Letouzey,
+        crossref        = "tphols2000",
+        title           = "Formalizing {S}t{\aa}lmarck's algorithm in {C}oq",
+        author          = "Pierre Letouzey and Laurent Th{\'e}ry",
+        pages           = "387--404"}
+
+@PROCEEDINGS{tphols2000,
+        editor          = "J. Harrison and M. Aagaard",
+        booktitle       = "Theorem Proving in Higher Order Logics:
+                           13th International Conference, TPHOLs 2000",
+        series          = "Lecture Notes in Computer Science",
+        volume          = 1869,
+        year            = 2000,
+        publisher       = "Springer-Verlag"}
\ No newline at end of file