path: root/doc/newfaq/fk.bib

%%%%%%% F %%%%%%%

@misc{fk:Practicals,
  author = {Florent Kirchner},
  title = "Programmation Tacticals",
  year  = 2003,
  note = "{\tt http://research.nianet.org/fm-at-nia/Practicals/}"
}

@mastersthesis{fk:DEA,
  author= {Florent Kirchner},
  title= "{Towards a Common Tactical Language : The Case of Coq and PVS}",
  school= {DEA Programmation : S�mantique, Preuves et Langages},
  year= 2003
}

@inproceedings{fk:strata2003,
  author= {Florent Kirchner},
  editor= {Mila Archer et al.},
  title= "{Coq Tacticals and PVS Strategies: A Small-Step Semantics}",
  pages= {69-83},
  booktitle= "{Design and Application of Strategies/Tactics in Higher Order Logics}",
  publisher= {NASA},
  month= "September",
  year= 2003
}

%%%%%%% Semantique %%%%%%%

@misc{Sem:cours,
  author = "Fran�ois Pottier",
  title =  "{Typage et Programmation}",
  year = "2002",
  howpublished = "Lecture notes",
  note = "DEA PSPL"
}

@inproceedings{Sem:Dubois,
  author    = {Catherine Dubois},
  editor    = {Mark Aagaard and
               John Harrison},
  title     = "{Proving ML Type Soundness Within Coq}",
  pages     = {126-144},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1869},
  year      = {2000},
  isbn      = {3-540-67863-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@techreport{Sem:Plotkin, 
author = {Gordon D. Plotkin}, 
institution = {Aarhus University}, 
number = {{DAIMI FN-19}}, 
title = {{A structural approach to operational semantics}}, 
year = {1981} 
} 

@article{Sem:RemyV98,
  author     = "Didier R{\'e}my and J{\'e}r{\^o}me Vouillon",
  title =        "Objective {ML}: 
                  An effective object-oriented extension to {ML}",
  journal =      "Theory And Practice of Object Systems",
  year =         1998,
  volume =    "4",
  number =    "1",
  pages =     "27--50",
  note =      {A preliminary version appeared in the proceedings
                  of the 24th ACM Conference on Principles
                  of Programming Languages, 1997}
}

@book{Sem:Winskel,
  AUTHOR      = {Winskel, Glynn},
  TITLE       = {The Formal Semantics of Programming Languages},
  NOTE        = {WIN g2 93:1 P-Ex},
  YEAR        = {1993},
  PUBLISHER   = {The MIT Press},
  SERIES      = {Foundations of Computing},
 }

@Article{Sem:WrightFelleisen,
  refkey =       "C1210",
  title =        "A Syntactic Approach to Type Soundness",
  author =       "Andrew K. Wright and Matthias Felleisen",
  pages =        "38--94",
  journal =      "Information and Computation",
  month =        "15~" # nov,
  year =         "1994",
  volume =       "115",
  number =       "1"
}

@inproceedings{Sem:Nipkow-MOD,
  author={Tobias Nipkow},
  title={Jinja: Towards a Comprehensive Formal Semantics for a
       {J}ava-like Language},
  booktitle={Proc.\ Marktobderdorf Summer School 2003},
  publisher={IOS Press},editor={H. Schwichtenberg and K. Spies},
  year=2003,
  note={To appear}
}

%%%%%%% Coq %%%%%%%

@techreport{Coq:man97,
  author = {B. Barras  and 
                              S. Boutin  and 
                              C. Cornes  and 
                              J. Courant and 
                              J.C. Filliatre and 
                              E. Gim\'enez    and 
                              H. Herbelin and 
                              G. Huet and 
                              C. Mu{\~n}oz and 
                              C. Murthy and
                              C. Parent and 
                              C. Paulin and 
                              A. Sa\"{\i}bi and 
                              B. Werner},
  institution = {INRIA},
  number = {0203},
  title = {{The Coq Proof Assistant Reference Manual -- Version V6.1}},
  year = {1997},
  month = {August},
}

@unpublished{Coq:e,
  author = {B. Barras  and 
                              S. Boutin  and 
                              C. Cornes  and 
                              J. Courant and 
                              J.C. Filliatre and 
                              E. Gim\'enez    and 
                              H. Herbelin and 
                              G. Huet and 
                              C. Mu{\~n}oz and 
                              C. Murthy and
                              C. Parent and 
                              C. Paulin and 
                              A. Sa\"{\i}bi and 
                              B. Werner},
  title = {{The Coq Proof Assistant Reference Manual -- Version 7.4}},
  year = {2003},
  note = {http://coq.inria.fr/doc/main.html}
}

@unpublished{Coq:coqart,
	author = "Y. Bertot and P. Casteran",
	title = "{Le Coq'Art}",
	url = "/Labri/Publications/Articles/coqart.ps.gz",
}

@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",
	SCHOOL = {Universit\'e Paris~6},
	YEAR = "2001",
        Type = {Th\`ese de Doctorat}
}

@techreport{Coq:gimenez-tut,
    author = "Eduardo Gimenez",
    title = "A Tutorial on Recursive Types in Coq",
    number = "RT-0221",
    pages = "42 p.",
    url = "citeseer.nj.nec.com/gimenez98tutorial.html" }

@phdthesis{Coq:Mun97,
	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},
        Number = {Unit\'e de recherche INRIA-Rocquencourt, TU-0488},
	YEAR = "1997",
        Note = {English version available as INRIA research report RR-3309},
        Type = {Th\`ese de Doctorat}
}

@PHDTHESIS{Coq: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},
}

@manual{Coq:Tutorial,
  AUTHOR = {G\'erard Huet, Gilles Kahn and Christine Paulin-Mohring},
  TITLE = {{The Coq Proof Assistant A Tutorial}},
  YEAR = 2004  
}

%%%%%%% PVS %%%%%%%

@manual{PVS:prover,
  title =        "{PVS} Prover Guide",
  author =       "N. Shankar and S. Owre and J. M. Rushby and D. W. J.
                 Stringer-Calvert",
  month =        sep,
  year =         "1999",
  organization = "Computer Science Laboratory, SRI International",
  address =      "Menlo Park, CA",
}

@techreport{PVS-Semantics:TR,
  TITLE = {The Formal Semantics of {PVS}},
  AUTHOR = {Sam Owre and Natarajan Shankar},
  NUMBER = {CR-1999-209321},
  INSTITUTION = {Computer Science Laboratory, SRI International},
  ADDRESS = {Menlo Park, CA},
  MONTH = may,
  YEAR = 1999,
}

@techreport{PVS-Tactics:DiVito,
  TITLE = {A {PVS} Prover Strategy Package for Common Manipulations},
  AUTHOR = {Ben L. Di Vito},
  NUMBER = {TM-2002-211647},
  INSTITUTION = {Langley Research Center},
  ADDRESS = {Hampton, VA},
  MONTH = apr,
  YEAR = 2002,
}

@misc{PVS-Tactics:cours,
  author = "C�sar Mu�oz",
  title = "Strategies in {PVS}",
  howpublished = "Lecture notes",
  note = "National Institute of Aerospace",
  year = 2002
}

@techreport{PVS-Tactics:field,
  author = "C. Mu{\~n}oz and M. Mayero",
  title = "Real Automation in the Field",
  institution = "ICASE-NASA Langley",
  number = "NASA/CR-2001-211271 Interim ICASE Report No. 39",
  month =  "dec",
  year = "2001"
}

%%%%%%% Autres Prouveurs %%%%%%%

@misc{ACL2:repNuPrl,
  author = "James L. Caldwell and John Cowles",
  title = "{Representing Nuprl Proof Objects in ACL2: toward a proof checker for Nuprl}",
  url = "http://www.cs.uwyo.edu/~jlc/papers/proof_checking.ps" }

@inproceedings{Elan:ckl-strat,
  author    = {H. Cirstea and C. Kirchner and L. Liquori},
  title     = "{Rewrite Strategies in the Rewriting Calculus}",
  booktitle = {WRLA'02},
  publisher = "{Elsevier Science B.V.}",
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {71},
  year      = {2003},
}

@book{LCF:GMW,
  author = {M. Gordon and R. Milner and C. Wadsworth},
  publisher = {sv},
  series = {lncs},
  volume = 78,
  title = {Edinburgh {LCF}: A Mechanized Logic of Computation},
  year = 1979
}

%%%%%%% LaTeX %%%%%%%

@manual{LaTeX:symb,
  title = "The Great, Big List of \LaTeX\ Symbols",
  author = "David Carlisle and Scott Pakin and Alexander Holt",
  month = feb,
  year = 2001,
}

@manual{LaTeX:intro,
  title = "The Not So Short Introduction to \LaTeX2e",
  author = "Tobias Oetiker",
  month = jan,
  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"}