@STRING{toappear="To appear"} @STRING{lncs="Lecture Notes in Computer Science"} @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} } @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} } @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 = {Springer-Verlag}, 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 = {LNCS, Springer-Verlag}, volume=1281, PS={http://pauillac.inria.fr/~boutin/public_w/submitTACS97.ps.gz}, year = {1997} } @PhdThesis{Bou97These, author = {S. Boutin}, title = {Réflexions sur les quotients}, school = {Paris 7}, year = 1997, type = {thèse d'Université}, 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{\'e}rieure} 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} } @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} } @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} } @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} } @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 = {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} } @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{\'e}currence implicite}, YEAR = {1994} } @MASTERSTHESIS{Del97, AUTHOR = {D. Delahaye}, MONTH = sep, SCHOOL = {DEA S{\'e}mantique, Preuves et Programmation, Paris 6}, TITLE = {Search2: un outil de recherche dans une biblioth\`eque de preuves Coq modulo isomorphismes}, YEAR = {1997} } @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} } @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} } @INPROCEEDINGS{Gim94, AUTHOR = {E. Gim\'enez}, BOOKTITLE = {Types'94 : Types for Proofs and Programs}, NOTE = {Extended version in LIP research report 95-07, ENS Lyon}, PUBLISHER = {Springer-Verlag}, SERIES = {LNCS}, TITLE = {{Codifying guarded definitions with recursive schemes}}, VOLUME = {996}, YEAR = {1994} } @TechReport{Gim98, author = {E. Giménez}, 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 = {Springer-Verlag}, YEAR = {1995} } @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} } @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 = {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} } @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} } @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 = {Springer-Verlag}, 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} } @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 = {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} } @BOOK{Moh97, AUTHOR = {C. 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{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{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} } @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} } @INPROCEEDINGS{Prasad93, AUTHOR = {K.V. Prasad}, BOOKTITLE = {{Proceedings of CONCUR'93}}, PUBLISHER = {Springer-Verlag}, SERIES = {LNCS}, TITLE = {{Programming with broadcasts}}, VOLUME = {715}, YEAR = {1993} } @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} } @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 = {Springer-Verlag}, 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} } @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} }