summaryrefslogtreecommitdiff
path: root/doc/RecTutorial/manbiblio.bib
diff options
context:
space:
mode:
Diffstat (limited to 'doc/RecTutorial/manbiblio.bib')
-rw-r--r--doc/RecTutorial/manbiblio.bib875
1 files changed, 875 insertions, 0 deletions
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}
+}
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 04:57:09 +0000