path: root/doc/biblio.bib

@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}
}