diff options
Diffstat (limited to 'doc/faq/fk.bib')
| -rw-r--r-- | doc/faq/fk.bib | 2221 |
1 files changed, 2221 insertions, 0 deletions
diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib new file mode 100644 index 00000000..d41ab7f0 --- /dev/null +++ b/doc/faq/fk.bib @@ -0,0 +1,2221 @@ +%%%%%%% 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} +} |