From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- doc/RecTutorial/manbiblio.bib | 875 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 875 insertions(+) create mode 100644 doc/RecTutorial/manbiblio.bib (limited to 'doc/RecTutorial/manbiblio.bib') diff --git a/doc/RecTutorial/manbiblio.bib b/doc/RecTutorial/manbiblio.bib new file mode 100644 index 00000000..099e3bbd --- /dev/null +++ b/doc/RecTutorial/manbiblio.bib @@ -0,0 +1,875 @@ + +@STRING{toappear="To appear"} +@STRING{lncs="Lecture Notes in Computer Science"} + +@TECHREPORT{RefManCoq, + AUTHOR = {Bruno~Barras, Samuel~Boutin, + Cristina~Cornes, Judicaël~Courant, Yann~Coscoy, David~Delahaye, + Daniel~de~Rauglaudre, Jean-Christophe~Filliâtre, Eduardo~Giménez, + Hugo~Herbelin, Gérard~Huet, Henri~Laulhère, César~Muñoz, + Chetan~Murthy, Catherine~Parent-Vigouroux, Patrick~Loiseleur, + Christine~Paulin-Mohring, Amokrane~Saïbi, Benjamin~Werner}, + INSTITUTION = {INRIA}, + TITLE = {{The Coq Proof Assistant Reference Manual -- Version V6.2}}, + YEAR = {1998} +} + +@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} +} + +@INPROCEEDINGS{EG94a, + AUTHOR = {E. Gim\'enez}, + EDITORS = {P. Dybjer and B. Nordstr\"om and J. Smith}, + BOOKTITLE = {Workshop on Types for Proofs and Programs}, + PAGES = {39-59}, + SERIES = {LNCS}, + NUMBER = {996}, + TITLE = {{Codifying guarded definitions with recursive schemes}}, + YEAR = {1994}, + PUBLISHER = {Springer-Verlag}, +} + +@INPROCEEDINGS{EG95a, + 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 = {Springer-Verlag}, + YEAR = {1995} +} + +@PhdThesis{EG96, + author = {E. Gim\'enez}, + title = {A Calculus of Infinite Constructions and its + application to the verification of communicating systems}, + school = {Ecole Normale Sup\'erieure de Lyon}, + year = {1996} +} + +@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} +} + +@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{Bee85, + AUTHOR = {M.J. Beeson}, + PUBLISHER = {Springer-Verlag}, + TITLE = {Foundations of Constructive Mathematics, Metamathematical Studies}, + YEAR = {1985} +} + +@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{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} +} + +@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{Leroy90, + AUTHOR = {X. Leroy}, + TITLE = {The {ZINC} experiment: an economical implementation +of the {ML} language}, + INSTITUTION = {INRIA}, + NUMBER = {117}, + YEAR = {1990} +} + +@BOOK{Caml, + AUTHOR = {P. Weis and X. Leroy}, + PUBLISHER = {InterEditions}, + TITLE = {Le langage Caml}, + YEAR = {1993} +} + +@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 = {Th. Coquand and G. Huet}, + ADDRESS = {Linz}, + BOOKTITLE = {EUROCAL'85}, + PUBLISHER = {Springer-Verlag}, + SERIES = {LNCS}, + TITLE = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}}, + VOLUME = {203}, + YEAR = {1985} +} + +@Misc{Bar98, + author = {B. Barras}, + title = {A formalisation of + \uppercase{B}urali-\uppercase{F}orti's paradox in Coq}, + howpublished = {Distributed within the bunch of contribution to the + Coq system}, + year = {1998}, + month = {March}, + note = {\texttt{http://pauillac.inria.fr/coq}} +} + + +@INPROCEEDINGS{CoHu85b, + AUTHOR = {Th. Coquand and G. 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 = {Th. Coquand and G. Huet}, + JOURNAL = {Information and Computation}, + NUMBER = {2/3}, + TITLE = {The {Calculus of Constructions}}, + VOLUME = {76}, + YEAR = {1988} +} + +@BOOK{Con86, + AUTHOR = {R.L. {Constable et al.}}, + PUBLISHER = {Prentice-Hall}, + TITLE = {{Implementing Mathematics with the Nuprl Proof Development System}}, + YEAR = {1986} +} + +@INPROCEEDINGS{CoPa89, + AUTHOR = {Th. Coquand and C. Paulin-Mohring}, + BOOKTITLE = {Proceedings of Colog'88}, + EDITOR = {P. Martin-L{\"o}f and G. Mints}, + PUBLISHER = {Springer-Verlag}, + SERIES = {LNCS}, + TITLE = {Inductively defined types}, + VOLUME = {417}, + YEAR = {1990} +} + +@PHDTHESIS{Coq85, + AUTHOR = {Th. Coquand}, + MONTH = jan, + SCHOOL = {Universit\'e Paris~7}, + TITLE = {Une Th\'eorie des Constructions}, + YEAR = {1985} +} + +@INPROCEEDINGS{Coq86, + AUTHOR = {Th. 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 = {Th. 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{Coq92, + AUTHOR = {Th. Coquand}, + BOOKTITLE = {in \cite{Bastad92}}, + TITLE = {{Pattern Matching with Dependent Types}}, + YEAR = {1992}, + crossref = {Bastad92} +} + +@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} +} + +@INPROCEEDINGS{Coquand93, + AUTHOR = {Th. Coquand}, + BOOKTITLE = {in \cite{Nijmegen93}}, + 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} +} + +@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} +} + +@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 Rendu 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 = {Springer-Verlag}, + 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{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} +} + +@UNPUBLISHED{Dow92a, + AUTHOR = {G. Dowek}, + NOTE = {To appear in Theoretical Computer Science}, + TITLE = {{The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}}, + YEAR = {1992} +} + +@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 {C}alcul des {P}r\'edicats {D}irect. {E}tude et impl\'ementation dans le syst\`eme {C}oq}, + 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} +} + +@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} +} + + +@TechReport{Gim98, + author = {E. Gim\'nez}, + title = {A Tutorial on Recursive Types in Coq}, + institution = {INRIA}, + year = {1998} +} + +@TECHREPORT{HKP97, + author = {G. Huet and G. Kahn and Ch. Paulin-Mohring}, + title = {The {Coq} Proof Assistant - A tutorial, Version 6.1}, + institution = {INRIA}, + type = {rapport technique}, + month = {Août}, + year = {1997}, + note = {Version révisée distribuée avec {Coq}}, + number = {204}, +} + +<<<<<<< biblio.bib + + +======= +>>>>>>> 1.4 +@INPROCEEDINGS{Gir70, + AUTHOR = {J.-Y. 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 = {J.-Y. 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 = {J.-Y. Girard and Y. Lafont and P. Taylor}, + PUBLISHER = {Cambridge University Press}, + SERIES = {Cambridge Tracts in Theoretical Computer Science 7}, + TITLE = {Proofs and Types}, + YEAR = {1989} +} + +@MASTERSTHESIS{Hir94, + AUTHOR = {D. Hirschkoff}, + MONTH = sep, + SCHOOL = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris}, + TITLE = {{Ecriture d'une tactique arithm\'etique pour le syst\`eme Coq}}, + YEAR = {1994} +} + +@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} +} + +@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} +} + +@INPROCEEDINGS{Hue87, + AUTHOR = {G. Huet}, + BOOKTITLE = {Programming of Future Generation Computers}, + EDITOR = {K. Fuchi and M. Nivat}, + NOTE = {Also in Proceedings of TAPSOFT87, LNCS 249, Springer-Verlag, 1987, pp 276--286}, + 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 = {Springer Verlag}, + 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} +} + +@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} +} + +@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} +} + +@BOOK{LE92, + EDITOR = {G. Huet and G. Plotkin}, + PUBLISHER = {Cambridge University Press}, + TITLE = {Logical Environments}, + YEAR = {1992} +} + +@INPROCEEDINGS{LePa94, + AUTHOR = {F. Leclerc and C. Paulin-Mohring}, + BOOKTITLE = {{Types for Proofs and Programs, Types' 93}}, + EDITOR = {H. Barendregt and T. Nipkow}, + PUBLISHER = {Springer-Verlag}, + SERIES = {LNCS}, + TITLE = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}}, + VOLUME = {806}, + YEAR = {1994} +} + +@BOOK{LF91, + EDITOR = {G. Huet and G. Plotkin}, + PUBLISHER = {Cambridge University Press}, + TITLE = {Logical Frameworks}, + YEAR = {1991} +} + +@BOOK{MaL84, + AUTHOR = {{P. Martin-L\"of}}, + PUBLISHER = {Bibliopolis}, + SERIES = {Studies in Proof Theory}, + TITLE = {Intuitionistic Type Theory}, + YEAR = {1984} +} + +@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} +} + +@ARTICLE{MaSi94, + AUTHOR = {P. Manoury and M. Simonot}, + JOURNAL = {TCS}, + TITLE = {Automatizing termination proof of recursively defined function}, + YEAR = {To appear} +} + +@TECHREPORT{maranget94, + AUTHOR = {L. Maranget}, + INSTITUTION = {INRIA}, + NUMBER = {2385}, + TITLE = {{Two Techniques for Compiling Lazy Pattern Matching}}, + YEAR = {1994} +} + +@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} +} + +@PHDTHESIS{Moh89b, + AUTHOR = {C. Paulin-Mohring}, + MONTH = jan, + SCHOOL = {{Universit\'e Paris 7}}, + TITLE = {Extraction de programmes dans le {Calcul des Constructions}}, + YEAR = {1989} +} + +@INPROCEEDINGS{Moh93, + AUTHOR = {C. 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 = {Springer-Verlag}, + SERIES = {LNCS}, + TITLE = {{Inductive Definitions in the System Coq - Rules and Properties}}, + YEAR = {1993} +} + +@MASTERSTHESIS{Mun94, + AUTHOR = {C. Mu\~noz}, + MONTH = sep, + SCHOOL = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, + TITLE = {D\'emonstration automatique dans la logique propositionnelle intuitionniste}, + YEAR = {1994} +} + +@BOOK{Nijmegen93, + EDITOR = {H. Barendregt and T. Nipkow}, + PUBLISHER = {Springer-Verlag}, + SERIES = {LNCS}, + TITLE = {Types for Proofs and Programs}, + VOLUME = {806}, + YEAR = {1994} +} + +@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 = {Springer-Verlag}, + SERIES = {LNCS}, + TITLE = {{ProPre : A Programming language with proofs}}, + YEAR = {1992} +} + +@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 = {Springer-Verlag}, + SERIES = {LNCS}, + TITLE = {{Synthesizing proofs from programs in +the Calculus of Inductive Constructions}}, + VOLUME = {947}, + YEAR = {1995} +} + +@ARTICLE{PaWe92, + AUTHOR = {C. Paulin-Mohring and B. Werner}, + JOURNAL = {Journal of Symbolic Computation}, + PAGES = {607--640}, + TITLE = {{Synthesis of ML programs in the system Coq}}, + VOLUME = {15}, + YEAR = {1993} +} + +@INPROCEEDINGS{Prasad93, + AUTHOR = {K.V. Prasad}, + BOOKTITLE = {{Proceedings of CONCUR'93}}, + PUBLISHER = {Springer-Verlag}, + SERIES = {LNCS}, + TITLE = {{Programming with broadcasts}}, + VOLUME = {715}, + YEAR = {1993} +} + +@INPROCEEDINGS{puel-suarez90, + AUTHOR = {L.Puel and A. Su\'arez}, + BOOKTITLE = {{Conference Lisp and Functional Programming}}, + SERIES = {ACM}, + PUBLISHER = {Springer-Verlag}, + TITLE = {{Compiling Pattern Matching by Term +Decomposition}}, + YEAR = {1990} +} + +@UNPUBLISHED{Rou92, + AUTHOR = {J. Rouyer}, + MONTH = aug, + NOTE = {To appear as a technical report}, + TITLE = {{D\'eveloppement 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{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} +} + +@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} +} + +@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} +} + +@PHDTHESIS{Wer94, + AUTHOR = {B. Werner}, + SCHOOL = {Universit\'e Paris 7}, + TITLE = {Une th\'eorie des constructions inductives}, + TYPE = {Th\`ese de Doctorat}, + YEAR = {1994} +} + + -- cgit v1.2.3