%%%%%%% FAQ %%%%%%% @book{ProofsTypes, Author="Girard, Jean-Yves and Yves Lafont and Paul Taylor", Title="Proofs and Types", Publisher="Cambrige Tracts in Theoretical Computer Science, Cambridge University Press", Year="1989" } @misc{Types:Dowek, author = "Gilles Dowek", title = "Th{\'e}orie des types", year = 2002, howpublished = "Lecture notes", url= "http://www.lix.polytechnique.fr/~dowek/Cours/theories_des_types.ps.gz" } @PHDTHESIS{EGThese, 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}, month = {December}, year = {1996}, } %%%%%%% 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 %%%%%%% @book{Coq:coqart, title = "Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions", author = "Yves Bertot and Pierre Castéran", publisher = "Springer Verlag", series = "Texts in Theoretical Computer Science. An EATCS series", year = 2004 } @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 Gim\'enez", 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 and 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, } @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 = {Christine 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"} @InCollection{howe, author = {Doug Howe}, title = {Computation Meta theory in Nuprl}, booktitle = {The Proceedings of the Ninth International Conference of Autom ated Deduction}, volume = {310}, editor = {E. Lusk and R. Overbeek}, publisher = {Springer-Verlag}, pages = {238--257}, year = {1988} } @TechReport{harrison, author = {John Harrison}, title = {Meta theory and Reflection in Theorem Proving:a Survey and Cri tique}, institution = {SRI International Cambridge Computer Science Research Center}, year = {1995}, number = {CRC-053} } @InCollection{cc, author = {Thierry Coquand and Gérard Huet}, title = {The Calculus of Constructions}, booktitle = {Information and Computation}, year = {1988}, volume = {76}, number = {2/3} } @InProceedings{coquandcci, author = {Thierry Coquand and Christine Paulin-Mohring}, title = {Inductively defined types}, booktitle = {Proceedings of Colog'88}, year = {1990}, editor = {P. Martin-Löf and G. Mints}, volume = {417}, series = {LNCS}, publisher = {Springer-Verlag} } @InProceedings{boutin, author = {Samuel Boutin}, title = {Using reflection to build efficient and certified decision pro cedures.}, booktitle = {Proceedings of TACS'97}, year = {1997}, editor = {M. Abadi and T. Ito}, volume = {1281}, series = {LNCS}, publisher = {Springer-Verlag} } @Manual{Coq:manual, title = {The Coq proof assistant reference manual}, author = {\mbox{The Coq development team}}, organization = {LogiCal Project}, note = {Version 8.0}, year = {2004}, url = "http://coq.inria.fr" } @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}"} @INPROCEEDINGS{Aud91, AUTHOR = {Ph. Audebaud}, BOOKTITLE = {Proceedings of the sixth Conf. on Logic in Computer Science.}, PUBLISHER = {IEEE}, TITLE = {Partial {Objects} in the {Calculus of Constructions}}, YEAR = {1991} } @PHDTHESIS{Aud92, AUTHOR = {Ph. Audebaud}, SCHOOL = {{Universit\'e} Bordeaux I}, TITLE = {Extension du Calcul des Constructions par Points fixes}, YEAR = {1992} } @INPROCEEDINGS{Audebaud92b, AUTHOR = {Ph. Audebaud}, BOOKTITLE = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}}, EDITOR = {{B. Nordstr\"om and K. Petersson and G. Plotkin}}, NOTE = {Also Research Report LIP-ENS-Lyon}, PAGES = {pp 21--34}, TITLE = {{CC+ : an extension of the Calculus of Constructions with fixpoints}}, YEAR = {1992} } @INPROCEEDINGS{Augustsson85, AUTHOR = {L. Augustsson}, TITLE = {{Compiling Pattern Matching}}, BOOKTITLE = {Conference Functional Programming and Computer Architecture}, YEAR = {1985} } @ARTICLE{BaCo85, AUTHOR = {J.L. Bates and R.L. Constable}, JOURNAL = {ACM transactions on Programming Languages and Systems}, TITLE = {Proofs as {Programs}}, VOLUME = {7}, YEAR = {1985} } @BOOK{Bar81, AUTHOR = {H.P. Barendregt}, PUBLISHER = {North-Holland}, TITLE = {The Lambda Calculus its Syntax and Semantics}, YEAR = {1981} } @TECHREPORT{Bar91, AUTHOR = {H. Barendregt}, INSTITUTION = {Catholic University Nijmegen}, NOTE = {In Handbook of Logic in Computer Science, Vol II}, NUMBER = {91-19}, TITLE = {Lambda {Calculi with Types}}, YEAR = {1991} } @ARTICLE{BeKe92, AUTHOR = {G. Bellin and J. Ketonen}, JOURNAL = {Theoretical Computer Science}, PAGES = {115--142}, TITLE = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation}, VOLUME = {95}, YEAR = {1992} } @BOOK{Bee85, AUTHOR = {M.J. Beeson}, PUBLISHER = SV, TITLE = {Foundations of Constructive Mathematics, Metamathematical Studies}, YEAR = {1985} } @BOOK{Bis67, AUTHOR = {E. Bishop}, PUBLISHER = {McGraw-Hill}, TITLE = {Foundations of Constructive Analysis}, YEAR = {1967} } @BOOK{BoMo79, AUTHOR = {R.S. Boyer and J.S. Moore}, KEY = {BoMo79}, PUBLISHER = {Academic Press}, SERIES = {ACM Monograph}, TITLE = {A computational logic}, YEAR = {1979} } @MASTERSTHESIS{Bou92, AUTHOR = {S. Boutin}, MONTH = sep, SCHOOL = {{Universit\'e Paris 7}}, TITLE = {Certification d'un compilateur {ML en Coq}}, YEAR = {1992} } @inproceedings{Bou97, title = {Using reflection to build efficient and certified decision procedure s}, author = {S. Boutin}, booktitle = {TACS'97}, editor = {Martin Abadi and Takahashi Ito}, publisher = SV, series = lncs, volume=1281, PS={http://pauillac.inria.fr/~boutin/public_w/submitTACS97.ps.gz}, year = {1997} } @PhdThesis{Bou97These, author = {S. Boutin}, title = {R\'eflexions sur les quotients}, school = {Paris 7}, year = 1997, type = {th\`ese d'Universit\'e}, month = apr } @ARTICLE{Bru72, AUTHOR = {N.J. de Bruijn}, JOURNAL = {Indag. Math.}, TITLE = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}}, VOLUME = {34}, YEAR = {1972} } @INCOLLECTION{Bru80, AUTHOR = {N.J. de Bruijn}, BOOKTITLE = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, EDITOR = {J.P. Seldin and J.R. Hindley}, PUBLISHER = {Academic Press}, TITLE = {A survey of the project {Automath}}, YEAR = {1980} } @TECHREPORT{COQ93, AUTHOR = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner}, INSTITUTION = {INRIA}, MONTH = may, NUMBER = {154}, TITLE = {{The Coq Proof Assistant User's Guide Version 5.8}}, YEAR = {1993} } @TECHREPORT{CPar93, AUTHOR = {C. Parent}, INSTITUTION = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, MONTH = oct, NOTE = {Also in~\cite{Nijmegen93}}, NUMBER = {93-29}, TITLE = {Developing certified programs in the system {Coq}- {The} {Program} tactic}, YEAR = {1993} } @PHDTHESIS{CPar95, AUTHOR = {C. Parent}, SCHOOL = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, TITLE = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}}, YEAR = {1995} } @BOOK{Caml, AUTHOR = {P. Weis and X. Leroy}, PUBLISHER = {InterEditions}, TITLE = {Le langage Caml}, YEAR = {1993} } @INPROCEEDINGS{ChiPotSimp03, AUTHOR = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson}, ADDRESS = {Berg en Dal, The Netherlands}, TITLE = {Mathematical Quotients and Quotient Types in Coq}, BOOKTITLE = {TYPES'02}, PUBLISHER = SV, SERIES = LNCS, VOLUME = {2646}, YEAR = {2003} } @TECHREPORT{CoC89, AUTHOR = {Projet Formel}, INSTITUTION = {INRIA}, NUMBER = {110}, TITLE = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}}, YEAR = {1989} } @INPROCEEDINGS{CoHu85a, AUTHOR = {Thierry Coquand and Gérard Huet}, ADDRESS = {Linz}, BOOKTITLE = {EUROCAL'85}, PUBLISHER = SV, SERIES = LNCS, TITLE = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}}, VOLUME = {203}, YEAR = {1985} } @INPROCEEDINGS{CoHu85b, AUTHOR = {Thierry Coquand and Gérard Huet}, BOOKTITLE = {Logic Colloquium'85}, EDITOR = {The Paris Logic Group}, PUBLISHER = {North-Holland}, TITLE = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}}, YEAR = {1987} } @ARTICLE{CoHu86, AUTHOR = {Thierry Coquand and Gérard Huet}, JOURNAL = {Information and Computation}, NUMBER = {2/3}, TITLE = {The {Calculus of Constructions}}, VOLUME = {76}, YEAR = {1988} } @INPROCEEDINGS{CoPa89, AUTHOR = {Thierry Coquand and Christine Paulin-Mohring}, BOOKTITLE = {Proceedings of Colog'88}, EDITOR = {P. Martin-L\"of and G. Mints}, PUBLISHER = SV, SERIES = LNCS, TITLE = {Inductively defined types}, VOLUME = {417}, YEAR = {1990} } @BOOK{Con86, AUTHOR = {R.L. {Constable et al.}}, PUBLISHER = {Prentice-Hall}, TITLE = {{Implementing Mathematics with the Nuprl Proof Development System}}, YEAR = {1986} } @PHDTHESIS{Coq85, AUTHOR = {Thierry Coquand}, MONTH = jan, SCHOOL = {Universit\'e Paris~7}, TITLE = {Une Th\'eorie des Constructions}, YEAR = {1985} } @INPROCEEDINGS{Coq86, AUTHOR = {Thierry Coquand}, ADDRESS = {Cambridge, MA}, BOOKTITLE = {Symposium on Logic in Computer Science}, PUBLISHER = {IEEE Computer Society Press}, TITLE = {{An Analysis of Girard's Paradox}}, YEAR = {1986} } @INPROCEEDINGS{Coq90, AUTHOR = {Thierry Coquand}, BOOKTITLE = {Logic and Computer Science}, EDITOR = {P. Oddifredi}, NOTE = {INRIA Research Report 1088, also in~\cite{CoC89}}, PUBLISHER = {Academic Press}, TITLE = {{Metamathematical Investigations of a Calculus of Constructions}}, YEAR = {1990} } @INPROCEEDINGS{Coq91, AUTHOR = {Thierry Coquand}, BOOKTITLE = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science}, TITLE = {{A New Paradox in Type Theory}}, MONTH = {August}, YEAR = {1991} } @INPROCEEDINGS{Coq92, AUTHOR = {Thierry Coquand}, TITLE = {{Pattern Matching with Dependent Types}}, YEAR = {1992}, crossref = {Bastad92} } @INPROCEEDINGS{Coquand93, AUTHOR = {Thierry Coquand}, TITLE = {{Infinite Objects in Type Theory}}, YEAR = {1993}, crossref = {Nijmegen93} } @MASTERSTHESIS{Cou94a, AUTHOR = {J. Courant}, MONTH = sep, SCHOOL = {DEA d'Informatique, ENS Lyon}, TITLE = {Explicitation de preuves par r\'ecurrence implicite}, YEAR = {1994} } @INPROCEEDINGS{Del99, author = "Delahaye, D.", title = "Information Retrieval in a Coq Proof Library using Type Isomorphisms", booktitle = {Proceedings of TYPES'99, L\"okeberg}, publisher = SV, series = lncs, year = "1999", url = "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# "{\sf TYPES99-SIsos.ps.gz}" } @INPROCEEDINGS{Del00, author = "Delahaye, D.", title = "A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}", booktitle = "Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island", publisher = SV, series = LNCS, volume = "1955", pages = "85--95", month = "November", year = "2000", url = "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# "{\sf LPAR2000-ltac.ps.gz}" } @INPROCEEDINGS{DelMay01, author = "Delahaye, D. and Mayero, M.", title = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels en {\Coq}}, booktitle = "Journ\'ees Francophones des Langages Applicatifs, Pontarlier", publisher = "INRIA", month = "Janvier", year = "2001", url = "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# "{\sf JFLA2000-Field.ps.gz}" } @TECHREPORT{Dow90, AUTHOR = {G. Dowek}, INSTITUTION = {INRIA}, NUMBER = {1283}, TITLE = {Naming and Scoping in a Mathematical Vernacular}, TYPE = {Research Report}, YEAR = {1990} } @ARTICLE{Dow91a, AUTHOR = {G. Dowek}, JOURNAL = {Compte-Rendus de l'Acad\'emie des Sciences}, NOTE = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors}, NUMBER = {12}, PAGES = {951--956}, TITLE = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, VOLUME = {I, 312}, YEAR = {1991} } @INPROCEEDINGS{Dow91b, AUTHOR = {G. Dowek}, BOOKTITLE = {Proceedings of Mathematical Foundation of Computer Science}, NOTE = {Also INRIA Research Report}, PAGES = {151--160}, PUBLISHER = SV, SERIES = LNCS, TITLE = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi}, VOLUME = {520}, YEAR = {1991} } @PHDTHESIS{Dow91c, AUTHOR = {G. Dowek}, MONTH = dec, SCHOOL = {Universit\'e Paris 7}, TITLE = {D\'emonstration automatique dans le Calcul des Constructions}, YEAR = {1991} } @article{Dow92a, AUTHOR = {G. Dowek}, TITLE = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}, YEAR = 1993, journal = tcs, volume = 107, number = 2, pages = {349-356} } @ARTICLE{Dow94a, AUTHOR = {G. Dowek}, JOURNAL = {Annals of Pure and Applied Logic}, VOLUME = {69}, PAGES = {135--155}, TITLE = {Third order matching is decidable}, YEAR = {1994} } @INPROCEEDINGS{Dow94b, AUTHOR = {G. Dowek}, BOOKTITLE = {Proceedings of the second international conference on typed lambda calculus and applications}, TITLE = {Lambda-calculus, Combinators and the Comprehension Schema}, YEAR = {1995} } @INPROCEEDINGS{Dyb91, AUTHOR = {P. Dybjer}, BOOKTITLE = {Logical Frameworks}, EDITOR = {G. Huet and G. Plotkin}, PAGES = {59--79}, PUBLISHER = {Cambridge University Press}, TITLE = {Inductive sets and families in {Martin-L{\"o}f's} Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, VOLUME = {14}, YEAR = {1991} } @ARTICLE{Dyc92, AUTHOR = {Roy Dyckhoff}, JOURNAL = {The Journal of Symbolic Logic}, MONTH = sep, NUMBER = {3}, TITLE = {Contraction-free sequent calculi for intuitionistic logic}, VOLUME = {57}, YEAR = {1992} } @MASTERSTHESIS{Fil94, 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. {\'E}tude et impl\'ementation dans le syst\`eme {\Coq}}, YEAR = {1994} } @TECHREPORT{Filliatre95, AUTHOR = {J.-C. Filli\^atre}, INSTITUTION = {LIP-ENS-Lyon}, TITLE = {A decision procedure for Direct Predicate Calculus}, TYPE = {Research report}, NUMBER = {96--25}, YEAR = {1995} } @Article{Filliatre03jfp, author = {J.-C. Filli{\^a}tre}, title = {Verification of Non-Functional Programs using Interpretations in Type Theory}, journal = jfp, volume = 13, number = 4, pages = {709--745}, month = jul, year = 2003, note = {[English translation of \cite{Filliatre99}]}, url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, topics = "team, lri", type_publi = "irevcomlec" } @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 = {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}} } @Unpublished{Filliatre99c, author = {J.-C. Filli\^atre}, title = {{Formal Proof of a Program: Find}}, month = {January}, year = 2000, note = {Submitted to \emph{Science of Computer Programming}}, url = {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}} } @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, url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}} } @UNPUBLISHED{Fle90, AUTHOR = {E. Fleury}, MONTH = jul, NOTE = {Rapport de Stage}, TITLE = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}}, YEAR = {1990} } @BOOK{Fourier, AUTHOR = {Jean-Baptiste-Joseph Fourier}, PUBLISHER = {Gauthier-Villars}, TITLE = {Fourier's method to solve linear inequations/equations systems.}, YEAR = {1890} } @INPROCEEDINGS{Gim94, AUTHOR = {Eduardo Gim\'enez}, BOOKTITLE = {Types'94 : Types for Proofs and Programs}, NOTE = {Extended version in LIP research report 95-07, ENS Lyon}, PUBLISHER = SV, SERIES = LNCS, TITLE = {Codifying guarded definitions with recursive schemes}, VOLUME = {996}, YEAR = {1994} } @TechReport{Gim98, author = {E. Gim\'enez}, title = {A Tutorial on Recursive Types in Coq}, institution = {INRIA}, year = 1998, month = mar } @INPROCEEDINGS{Gimenez95b, AUTHOR = {E. Gim\'enez}, BOOKTITLE = {Workshop on Types for Proofs and Programs}, SERIES = LNCS, NUMBER = {1158}, PAGES = {135-152}, TITLE = {An application of co-Inductive types in Coq: verification of the Alternating Bit Protocol}, EDITORS = {S. Berardi and M. Coppo}, PUBLISHER = SV, YEAR = {1995} } @INPROCEEDINGS{Gir70, AUTHOR = {Jean-Yves Girard}, BOOKTITLE = {Proceedings of the 2nd Scandinavian Logic Symposium}, PUBLISHER = {North-Holland}, TITLE = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types}, YEAR = {1970} } @PHDTHESIS{Gir72, AUTHOR = {Jean-Yves Girard}, SCHOOL = {Universit\'e Paris~7}, TITLE = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur}, YEAR = {1972} } @BOOK{Gir89, AUTHOR = {Jean-Yves Girard and Yves Lafont and Paul Taylor}, PUBLISHER = {Cambridge University Press}, SERIES = {Cambridge Tracts in Theoretical Computer Science 7}, TITLE = {Proofs and Types}, YEAR = {1989} } @TechReport{Har95, author = {John Harrison}, title = {Metatheory and Reflection in Theorem Proving: A Survey and Critique}, institution = {SRI International Cambridge Computer Science Research Centre,}, year = 1995, type = {Technical Report}, number = {CRC-053}, abstract = {http://www.cl.cam.ac.uk/users/jrh/papers.html} } @MASTERSTHESIS{Hir94, AUTHOR = {Daniel Hirschkoff}, MONTH = sep, SCHOOL = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris}, TITLE = {{\'E}criture d'une tactique arithm\'etique pour le syst\`eme {\Coq}}, YEAR = {1994} } @INPROCEEDINGS{HofStr98, AUTHOR = {Martin Hofmann and Thomas Streicher}, TITLE = {The groupoid interpretation of type theory}, BOOKTITLE = {Proceedings of the meeting Twenty-five years of constructive type theory}, PUBLISHER = {Oxford University Press}, YEAR = {1998} } @INCOLLECTION{How80, AUTHOR = {W.A. Howard}, BOOKTITLE = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, EDITOR = {J.P. Seldin and J.R. Hindley}, NOTE = {Unpublished 1969 Manuscript}, PUBLISHER = {Academic Press}, TITLE = {The Formulae-as-Types Notion of Constructions}, YEAR = {1980} } @InProceedings{Hue87tapsoft, author = {G. Huet}, title = {Programming of Future Generation Computers}, booktitle = {Proceedings of TAPSOFT87}, series = LNCS, volume = 249, pages = {276--286}, year = 1987, publisher = SV } @INPROCEEDINGS{Hue87, AUTHOR = {G. Huet}, BOOKTITLE = {Programming of Future Generation Computers}, EDITOR = {K. Fuchi and M. Nivat}, NOTE = {Also in \cite{Hue87tapsoft}}, PUBLISHER = {Elsevier Science}, TITLE = {Induction Principles Formalized in the {Calculus of Constructions}}, YEAR = {1988} } @INPROCEEDINGS{Hue88, AUTHOR = {G. Huet}, BOOKTITLE = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, EDITOR = {R. Narasimhan}, NOTE = {Also in~\cite{CoC89}}, PUBLISHER = {World Scientific Publishing}, TITLE = {{The Constructive Engine}}, YEAR = {1989} } @BOOK{Hue89, EDITOR = {G. Huet}, PUBLISHER = {Addison-Wesley}, SERIES = {The UT Year of Programming Series}, TITLE = {Logical Foundations of Functional Programming}, YEAR = {1989} } @INPROCEEDINGS{Hue92, AUTHOR = {G. Huet}, BOOKTITLE = {Proceedings of 12th FST/TCS Conference, New Delhi}, PAGES = {229--240}, PUBLISHER = SV, SERIES = LNCS, TITLE = {The Gallina Specification Language : A case study}, VOLUME = {652}, YEAR = {1992} } @ARTICLE{Hue94, AUTHOR = {G. Huet}, JOURNAL = {J. Functional Programming}, PAGES = {371--394}, PUBLISHER = {Cambridge University Press}, TITLE = {Residual theory in $\lambda$-calculus: a formal development}, VOLUME = {4,3}, YEAR = {1994} } @INCOLLECTION{HuetLevy79, AUTHOR = {G. Huet and J.-J. L\'{e}vy}, TITLE = {Call by Need Computations in Non-Ambigous Linear Term Rewriting Systems}, NOTE = {Also research report 359, INRIA, 1979}, BOOKTITLE = {Computational Logic, Essays in Honor of Alan Robinson}, EDITOR = {J.-L. Lassez and G. Plotkin}, PUBLISHER = {The MIT press}, YEAR = {1991} } @ARTICLE{KeWe84, AUTHOR = {J. Ketonen and R. Weyhrauch}, JOURNAL = {Theoretical Computer Science}, PAGES = {297--307}, TITLE = {A decidable fragment of {P}redicate {C}alculus}, VOLUME = {32}, YEAR = {1984} } @BOOK{Kle52, AUTHOR = {S.C. Kleene}, PUBLISHER = {North-Holland}, SERIES = {Bibliotheca Mathematica}, TITLE = {Introduction to Metamathematics}, YEAR = {1952} } @BOOK{Kri90, AUTHOR = {J.-L. Krivine}, PUBLISHER = {Masson}, SERIES = {Etudes et recherche en informatique}, TITLE = {Lambda-calcul {types et mod\`eles}}, YEAR = {1990} } @BOOK{LE92, EDITOR = {G. Huet and G. Plotkin}, PUBLISHER = {Cambridge University Press}, TITLE = {Logical Environments}, YEAR = {1992} } @BOOK{LF91, EDITOR = {G. Huet and G. Plotkin}, PUBLISHER = {Cambridge University Press}, TITLE = {Logical Frameworks}, YEAR = {1991} } @ARTICLE{Laville91, AUTHOR = {A. Laville}, TITLE = {Comparison of Priority Rules in Pattern Matching and Term Rewriting}, JOURNAL = {Journal of Symbolic Computation}, VOLUME = {11}, PAGES = {321--347}, YEAR = {1991} } @INPROCEEDINGS{LePa94, AUTHOR = {F. Leclerc and C. Paulin-Mohring}, BOOKTITLE = {{Types for Proofs and Programs, Types' 93}}, EDITOR = {H. Barendregt and T. Nipkow}, PUBLISHER = SV, SERIES = {LNCS}, TITLE = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}}, VOLUME = {806}, YEAR = {1994} } @TECHREPORT{Leroy90, AUTHOR = {X. Leroy}, TITLE = {The {ZINC} experiment: an economical implementation of the {ML} language}, INSTITUTION = {INRIA}, NUMBER = {117}, YEAR = {1990} } @INPROCEEDINGS{Let02, author = {P. Letouzey}, title = {A New Extraction for Coq}, booktitle = {Proceedings of the TYPES'2002 workshop}, year = 2002, note = {to appear}, url = {draft at \url{http://www.lri.fr/~letouzey/download/extraction2002.ps.gz}} } @BOOK{MaL84, AUTHOR = {{P. Martin-L\"of}}, PUBLISHER = {Bibliopolis}, SERIES = {Studies in Proof Theory}, TITLE = {Intuitionistic Type Theory}, YEAR = {1984} } @ARTICLE{MaSi94, AUTHOR = {P. Manoury and M. Simonot}, JOURNAL = {TCS}, TITLE = {Automatizing termination proof of recursively defined function}, YEAR = {To appear} } @INPROCEEDINGS{Moh89a, AUTHOR = {Christine 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} } @PHDTHESIS{Moh89b, AUTHOR = {Christine Paulin-Mohring}, MONTH = jan, SCHOOL = {{Universit\'e Paris 7}}, TITLE = {Extraction de programmes dans le {Calcul des Constructions}}, YEAR = {1989} } @INPROCEEDINGS{Moh93, AUTHOR = {Christine Paulin-Mohring}, BOOKTITLE = {Proceedings of the conference Typed Lambda Calculi and Applications}, EDITOR = {M. Bezem and J.-F. Groote}, NOTE = {Also LIP research report 92-49, ENS Lyon}, NUMBER = {664}, PUBLISHER = SV, SERIES = {LNCS}, TITLE = {{Inductive Definitions in the System Coq - Rules and Properties}}, YEAR = {1993} } @BOOK{Moh97, AUTHOR = {Christine Paulin-Mohring}, MONTH = jan, PUBLISHER = {{ENS Lyon}}, TITLE = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}}, YEAR = {1997} } @MASTERSTHESIS{Mun94, AUTHOR = {C. Mu{\~n}oz}, MONTH = sep, SCHOOL = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, TITLE = {D\'emonstration automatique dans la logique propositionnelle intuitionniste}, YEAR = {1994} } @PHDTHESIS{Mun97d, AUTHOR = "C. 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}, YEAR = "1997", Note = {Version en anglais disponible comme rapport de recherche INRIA RR-3309}, Type = {Th\`ese de Doctorat} } @BOOK{NoPS90, AUTHOR = {B. {Nordstr\"om} and K. Peterson and J. Smith}, BOOKTITLE = {Information Processing 83}, PUBLISHER = {Oxford Science Publications}, SERIES = {International Series of Monographs on Computer Science}, TITLE = {Programming in {Martin-L\"of's} Type Theory}, YEAR = {1990} } @ARTICLE{Nor88, AUTHOR = {B. {Nordstr\"om}}, JOURNAL = {BIT}, TITLE = {Terminating General Recursion}, VOLUME = {28}, YEAR = {1988} } @BOOK{Odi90, EDITOR = {P. Odifreddi}, PUBLISHER = {Academic Press}, TITLE = {Logic and Computer Science}, YEAR = {1990} } @INPROCEEDINGS{PaMS92, AUTHOR = {M. Parigot and P. Manoury and M. Simonot}, ADDRESS = {St. Petersburg, Russia}, BOOKTITLE = {Logic Programming and automated reasoning}, EDITOR = {A. Voronkov}, MONTH = jul, NUMBER = {624}, PUBLISHER = SV, SERIES = {LNCS}, TITLE = {{ProPre : A Programming language with proofs}}, YEAR = {1992} } @ARTICLE{PaWe92, AUTHOR = {Christine Paulin-Mohring and Benjamin Werner}, JOURNAL = {Journal of Symbolic Computation}, PAGES = {607--640}, TITLE = {{Synthesis of ML programs in the system Coq}}, VOLUME = {15}, YEAR = {1993} } @ARTICLE{Par92, AUTHOR = {M. Parigot}, JOURNAL = {Theoretical Computer Science}, NUMBER = {2}, PAGES = {335--356}, TITLE = {{Recursive Programming with Proofs}}, VOLUME = {94}, YEAR = {1992} } @INPROCEEDINGS{Parent95b, AUTHOR = {C. Parent}, BOOKTITLE = {{Mathematics of Program Construction'95}}, PUBLISHER = SV, SERIES = {LNCS}, TITLE = {{Synthesizing proofs from programs in the Calculus of Inductive Constructions}}, VOLUME = {947}, YEAR = {1995} } @INPROCEEDINGS{Prasad93, AUTHOR = {K.V. Prasad}, BOOKTITLE = {{Proceedings of CONCUR'93}}, PUBLISHER = SV, SERIES = {LNCS}, TITLE = {{Programming with broadcasts}}, VOLUME = {715}, YEAR = {1993} } @BOOK{RC95, author = "di~Cosmo, R.", title = "Isomorphisms of Types: from $\lambda$-calculus to information retrieval and language design", series = "Progress in Theoretical Computer Science", publisher = "Birkhauser", year = "1995", note = "ISBN-0-8176-3763-X" } @TECHREPORT{Rou92, AUTHOR = {J. Rouyer}, INSTITUTION = {INRIA}, MONTH = nov, NUMBER = {1795}, TITLE = {{D{\'e}veloppement de l'Algorithme d'Unification dans le Calcul des Constructions}}, YEAR = {1992} } @TECHREPORT{Saibi94, AUTHOR = {A. Sa\"{\i}bi}, INSTITUTION = {INRIA}, MONTH = dec, NUMBER = {2345}, TITLE = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}}, YEAR = {1994} } @MASTERSTHESIS{Ter92, AUTHOR = {D. Terrasse}, MONTH = sep, SCHOOL = {IARFA}, TITLE = {{Traduction de TYPOL en COQ. Application \`a Mini ML}}, YEAR = {1992} } @TECHREPORT{ThBeKa92, AUTHOR = {L. Th\'ery and Y. Bertot and G. Kahn}, INSTITUTION = {INRIA Sophia}, MONTH = may, NUMBER = {1684}, TITLE = {Real theorem provers deserve real user-interfaces}, TYPE = {Research Report}, YEAR = {1992} } @BOOK{TrDa89, AUTHOR = {A.S. Troelstra and D. van Dalen}, PUBLISHER = {North-Holland}, SERIES = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123}, TITLE = {Constructivism in Mathematics, an introduction}, YEAR = {1988} } @PHDTHESIS{Wer94, AUTHOR = {B. Werner}, SCHOOL = {Universit\'e Paris 7}, TITLE = {Une th\'eorie des constructions inductives}, TYPE = {Th\`ese de Doctorat}, YEAR = {1994} } @PHDTHESIS{Bar99, AUTHOR = {B. Barras}, SCHOOL = {Universit\'e Paris 7}, TITLE = {Auto-validation d'un système de preuves avec familles inductives}, TYPE = {Th\`ese de Doctorat}, YEAR = {1999} } @UNPUBLISHED{ddr98, AUTHOR = {D. de Rauglaudre}, TITLE = {Camlp4 version 1.07.2}, YEAR = {1998}, NOTE = {In Camlp4 distribution} } @ARTICLE{dowek93, AUTHOR = {G. Dowek}, TITLE = {{A Complete Proof Synthesis Method for the Cube of Type Systems}}, JOURNAL = {Journal Logic Computation}, VOLUME = {3}, NUMBER = {3}, PAGES = {287--315}, MONTH = {June}, YEAR = {1993} } @INPROCEEDINGS{manoury94, AUTHOR = {P. Manoury}, TITLE = {{A User's Friendly Syntax to Define Recursive Functions as Typed $\lambda-$Terms}}, BOOKTITLE = {{Types for Proofs and Programs, TYPES'94}}, SERIES = {LNCS}, VOLUME = {996}, MONTH = jun, YEAR = {1994} } @TECHREPORT{maranget94, AUTHOR = {L. Maranget}, INSTITUTION = {INRIA}, NUMBER = {2385}, TITLE = {{Two Techniques for Compiling Lazy Pattern Matching}}, YEAR = {1994} } @INPROCEEDINGS{puel-suarez90, AUTHOR = {L.Puel and A. Su\'arez}, BOOKTITLE = {{Conference Lisp and Functional Programming}}, SERIES = {ACM}, PUBLISHER = SV, TITLE = {{Compiling Pattern Matching by Term Decomposition}}, YEAR = {1990} } @MASTERSTHESIS{saidi94, AUTHOR = {H. Saidi}, MONTH = sep, SCHOOL = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, TITLE = {R\'esolution d'\'equations dans le syst\`eme T de G\"odel}, YEAR = {1994} } @misc{streicher93semantical, author = "T. Streicher", title = "Semantical Investigations into Intensional Type Theory", note = "Habilitationsschrift, LMU Munchen.", year = "1993" } @Misc{Pcoq, author = {Lemme Team}, title = {Pcoq a graphical user-interface for {Coq}}, note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} } @Misc{ProofGeneral, author = {David Aspinall}, title = {Proof General}, note = {\url{http://proofgeneral.inf.ed.ac.uk/}} } @Book{CoqArt, author = {Yves bertot and Pierre Castéran}, title = {Coq'Art}, publisher = {Springer-Verlag}, year = 2004, note = {To appear} } @INCOLLECTION{wadler87, AUTHOR = {P. Wadler}, TITLE = {Efficient Compilation of Pattern Matching}, BOOKTITLE = {The Implementation of Functional Programming Languages}, EDITOR = {S.L. Peyton Jones}, PUBLISHER = {Prentice-Hall}, YEAR = {1987} } @COMMENT{cross-references, must be at end} @BOOK{Bastad92, EDITOR = {B. Nordstr\"om and K. Petersson and G. Plotkin}, PUBLISHER = {Available by ftp at site ftp.inria.fr}, TITLE = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}, YEAR = {1992} } @BOOK{Nijmegen93, EDITOR = {H. Barendregt and T. Nipkow}, PUBLISHER = SV, SERIES = LNCS, TITLE = {Types for Proofs and Programs}, VOLUME = {806}, YEAR = {1994} } @PHDTHESIS{Luo90, AUTHOR = {Z. Luo}, TITLE = {An Extended Calculus of Constructions}, SCHOOL = {University of Edinburgh}, YEAR = {1990} }