@string{jfp = "Journal of Functional Programming"}
@STRING{lncs="Lecture Notes in Computer Science"}
@STRING{lnai="Lecture Notes in Artificial Intelligence"}
@string{SV = "{Sprin\-ger-Verlag}"}

@INPROCEEDINGS{Aud91,
        AUTHOR             = {Ph. Audebaud},
        BOOKTITLE          = {Proceedings of the sixth Conf. on Logic in Computer Science.},
        PUBLISHER          = {IEEE},
        TITLE              = {Partial {Objects} in the {Calculus of Constructions}},
        YEAR               = {1991}
}

@PHDTHESIS{Aud92,
        AUTHOR             = {Ph. Audebaud},
        SCHOOL             = {{Universit\'e} Bordeaux I},
        TITLE              = {Extension du Calcul des Constructions par Points fixes},
        YEAR               = {1992}
}

@INPROCEEDINGS{Audebaud92b,
        AUTHOR             = {Ph. Audebaud},
        BOOKTITLE          = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}},
        EDITOR             = {{B. Nordstr\"om and K. Petersson and G. Plotkin}},
        NOTE               = {Also Research Report LIP-ENS-Lyon},
        PAGES              = {pp 21--34},
        TITLE              = {{CC+ : an extension of the Calculus of Constructions with fixpoints}},
        YEAR               = {1992}
}

@INPROCEEDINGS{Augustsson85,
        AUTHOR             = {L. Augustsson},
        TITLE              = {{Compiling Pattern Matching}},
        BOOKTITLE          = {Conference Functional Programming and
Computer Architecture},
        YEAR               = {1985}
}

@ARTICLE{BaCo85,
        AUTHOR             = {J.L. Bates and R.L. Constable},
        JOURNAL            = {ACM transactions on Programming Languages and Systems},
        TITLE              = {Proofs as {Programs}},
        VOLUME             = {7},
        YEAR               = {1985}
}

@BOOK{Bar81,
        AUTHOR             = {H.P. Barendregt},
        PUBLISHER          = {North-Holland},
        TITLE              = {The Lambda Calculus its Syntax and Semantics},
        YEAR               = {1981}
}

@TECHREPORT{Bar91,
        AUTHOR             = {H. Barendregt},
        INSTITUTION        = {Catholic University Nijmegen},
        NOTE               = {In Handbook of Logic in Computer Science, Vol II},
        NUMBER             = {91-19},
        TITLE              = {Lambda {Calculi with Types}},
        YEAR               = {1991}
}

@ARTICLE{BeKe92,
        AUTHOR             = {G. Bellin and J. Ketonen},
        JOURNAL            = {Theoretical Computer Science},
        PAGES              = {115--142},
        TITLE              = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation},
        VOLUME             = {95},
        YEAR               = {1992}
}

@BOOK{Bee85,
        AUTHOR             = {M.J. Beeson},
        PUBLISHER          = SV,
        TITLE              = {Foundations of Constructive Mathematics, Metamathematical Studies},
        YEAR               = {1985}
}

@BOOK{Bis67,
        AUTHOR             = {E. Bishop},
        PUBLISHER          = {McGraw-Hill},
        TITLE              = {Foundations of Constructive Analysis},
        YEAR               = {1967}
}

@BOOK{BoMo79,
        AUTHOR             = {R.S. Boyer and J.S. Moore},
        KEY                = {BoMo79},
        PUBLISHER          = {Academic Press},
        SERIES             = {ACM Monograph},
        TITLE              = {A computational logic},
        YEAR               = {1979}
}

@MASTERSTHESIS{Bou92,
        AUTHOR             = {S. Boutin},
        MONTH              = sep,
        SCHOOL             = {{Universit\'e Paris 7}},
        TITLE              = {Certification d'un compilateur {ML en Coq}},
        YEAR               = {1992}
}

@INPROCEEDINGS{Bou97,
   TITLE       = {Using reflection to build efficient and certified decision procedure
s},
   AUTHOR      = {S. Boutin},
   BOOKTITLE   = {TACS'97},
   EDITOR      = {Martin Abadi and Takahashi Ito},
   PUBLISHER   = SV,
   SERIES      = lncs,
   VOLUME      = 1281, 
   YEAR        = {1997}
}

@PHDTHESIS{Bou97These,
  AUTHOR       = {S. Boutin},
  TITLE        = {R\'eflexions sur les quotients},
  SCHOOL       = {Paris 7},
  YEAR         = 1997,
  TYPE         = {th\`ese d'Universit\'e},
  MONTH        = apr
}

@ARTICLE{Bru72,
        AUTHOR             = {N.J. de Bruijn},
        JOURNAL            = {Indag. Math.},
        TITLE              = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}},
        VOLUME             = {34},
        YEAR               = {1972}
}


@INCOLLECTION{Bru80,
        AUTHOR             = {N.J. de Bruijn},
        BOOKTITLE          = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
        EDITOR             = {J.P. Seldin and J.R. Hindley},
        PUBLISHER          = {Academic Press},
        TITLE              = {A survey of the project {Automath}},
        YEAR               = {1980}
}

@TECHREPORT{COQ93,
        AUTHOR             = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner},
        INSTITUTION        = {INRIA},
        MONTH              = may,
        NUMBER             = {154},
        TITLE              = {{The Coq Proof Assistant User's Guide Version 5.8}},
        YEAR               = {1993}
}

@TECHREPORT{COQ02,
        AUTHOR             = {The Coq Development Team},
        INSTITUTION        = {INRIA},
        MONTH              = Feb,
        NUMBER             = {255},
        TITLE              = {{The Coq Proof Assistant Reference Manual Version 7.2}},
        YEAR               = {2002}
}

@TECHREPORT{CPar93,
        AUTHOR             = {C. Parent},
        INSTITUTION        = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
        MONTH              = oct,
        NOTE               = {Also in~\cite{Nijmegen93}},
        NUMBER             = {93-29},
        TITLE              = {Developing certified programs in the system {Coq}- {The} {Program} tactic},
        YEAR               = {1993}
}

@PHDTHESIS{CPar95,
        AUTHOR             = {C. Parent},
        SCHOOL             = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
        TITLE              = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}},
        YEAR               = {1995}
}

@BOOK{Caml,
        AUTHOR             = {P. Weis and X. Leroy},
        PUBLISHER          = {InterEditions},
        TITLE              = {Le langage Caml},
        YEAR               = {1993}
}

@INPROCEEDINGS{ChiPotSimp03,
  AUTHOR    = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson},
  ADDRESS   = {Berg en Dal, The Netherlands},
  TITLE     = {Mathematical Quotients and Quotient Types in Coq},
  BOOKTITLE = {TYPES'02},
  PUBLISHER = SV,
  SERIES    = LNCS,
  VOLUME    = {2646},
  YEAR      = {2003}
}

@TECHREPORT{CoC89,
        AUTHOR             = {Projet Formel},
        INSTITUTION        = {INRIA},
        NUMBER             = {110},
        TITLE              = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}},
        YEAR               = {1989}
}

@INPROCEEDINGS{CoHu85a,
        AUTHOR             = {Th. Coquand and G. Huet},
        ADDRESS            = {Linz},
        BOOKTITLE          = {EUROCAL'85},
        PUBLISHER          = SV,
        SERIES             = LNCS,
        TITLE              = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}},
        VOLUME             = {203},
        YEAR               = {1985}
}

@INPROCEEDINGS{CoHu85b,
        AUTHOR             = {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\"of and G. Mints},
        PUBLISHER          = SV,
        SERIES             = LNCS,
        TITLE              = {Inductively defined types},
        VOLUME             = {417},
        YEAR               = {1990}
}

@BOOK{Con86,
        AUTHOR             = {R.L. {Constable et al.}},
        PUBLISHER          = {Prentice-Hall},
        TITLE              = {{Implementing Mathematics with the Nuprl Proof Development System}},
        YEAR               = {1986}
}

@PHDTHESIS{Coq85,
        AUTHOR             = {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{Coq91,
        AUTHOR             = {Th. Coquand},
        BOOKTITLE          = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science},
        TITLE              = {{A New Paradox in Type Theory}},
        MONTH              = {August},
        YEAR               = {1991}
}

@INPROCEEDINGS{Coq92,
        AUTHOR             = {Th. Coquand},
        TITLE              = {{Pattern Matching with Dependent Types}},
        YEAR               = {1992},
        crossref = {Bastad92}
}

@INPROCEEDINGS{Coquand93,
        AUTHOR             = {Th. Coquand},
        TITLE              = {{Infinite Objects in Type Theory}},
        YEAR               = {1993},
        crossref = {Nijmegen93}
}

@PHDTHESIS{Cor97,
        AUTHOR             = {C. Cornes},
        MONTH              = nov,
        SCHOOL             = {{Universit\'e Paris 7}},
        TITLE              = {Conception d'un langage de haut niveau de représentation de preuves},
        TYPE               = {Th\`ese de Doctorat},
        YEAR               = {1997}
}

@MASTERSTHESIS{Cou94a,
        AUTHOR             = {J. Courant},
        MONTH              = sep,
        SCHOOL             = {DEA d'Informatique, ENS Lyon},
        TITLE              = {Explicitation de preuves par r\'ecurrence implicite},
        YEAR               = {1994}
}

@INPROCEEDINGS{Del99,
  author    = "Delahaye, D.",
  title     = "Information Retrieval in a Coq Proof Library using
               Type Isomorphisms",
  booktitle = {Proceedings of TYPES'99, L\"okeberg},
  publisher = SV,
  series = lncs,
  year      = "1999",
  url      =
    "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
    "{\sf TYPES99-SIsos.ps.gz}"
}

@INPROCEEDINGS{Del00,
  author    = "Delahaye, D.",
  title     = "A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}",
  booktitle = "Proceedings of Logic for Programming and Automated Reasoning
               (LPAR), Reunion Island",
  publisher = SV,
  series =  LNCS,
  volume    = "1955",
  pages     = "85--95",
  month     = "November",
  year      = "2000",
  url      =
    "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
    "{\sf LPAR2000-ltac.ps.gz}"
}

@INPROCEEDINGS{DelMay01,
  author    = "Delahaye, D. and Mayero, M.",
  title     = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels
               en {\Coq}},
  booktitle = "Journ\'ees Francophones des Langages Applicatifs, Pontarlier",
  publisher = "INRIA",
  month     = "Janvier",
  year      = "2001",
  url      =
    "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
    "{\sf JFLA2000-Field.ps.gz}"
}

@TECHREPORT{Dow90,
        AUTHOR             = {G. Dowek},
        INSTITUTION        = {INRIA},
        NUMBER             = {1283},
        TITLE              = {Naming and Scoping in a Mathematical Vernacular},
        TYPE               = {Research Report},
        YEAR               = {1990}
}

@ARTICLE{Dow91a,
        AUTHOR             = {G. Dowek},
        JOURNAL            = {Compte-Rendus de l'Acad\'emie des Sciences},
        NOTE               = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors},
        NUMBER             = {12},
        PAGES              = {951--956},
        TITLE              = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, 
        VOLUME             = {I, 312},
        YEAR               = {1991}
}		  

@INPROCEEDINGS{Dow91b,
        AUTHOR             = {G. Dowek},
        BOOKTITLE          = {Proceedings of Mathematical Foundation of Computer Science},
        NOTE               = {Also INRIA Research Report},
        PAGES              = {151--160},
        PUBLISHER          = SV,
        SERIES             = LNCS,
        TITLE              = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi},
        VOLUME             = {520},
        YEAR               = {1991}
}
                  
@PHDTHESIS{Dow91c,
        AUTHOR             = {G. Dowek},
        MONTH              = dec,
        SCHOOL             = {Universit\'e Paris 7},
        TITLE              = {D\'emonstration automatique dans le Calcul des Constructions},
        YEAR               = {1991}
}

@article{Dow92a,
        AUTHOR             = {G. Dowek},
        TITLE              = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable},
        YEAR               = 1993,
        journal = tcs,
        volume = 107,
        number = 2,
        pages = {349-356}
}


@ARTICLE{Dow94a,
        AUTHOR             = {G. Dowek},
        JOURNAL            = {Annals of Pure and Applied Logic},
        VOLUME             = {69},
        PAGES              = {135--155},
        TITLE              = {Third order matching is decidable},
        YEAR               = {1994}
}

@INPROCEEDINGS{Dow94b,
        AUTHOR             = {G. Dowek},
        BOOKTITLE          = {Proceedings of the second international conference on typed lambda calculus and applications},
        TITLE              = {Lambda-calculus, Combinators and the Comprehension Schema},
        YEAR               = {1995}
}

@INPROCEEDINGS{Dyb91,
        AUTHOR             = {P. Dybjer},
        BOOKTITLE          = {Logical Frameworks},
        EDITOR             = {G. Huet and G. Plotkin},
        PAGES              = {59--79},
        PUBLISHER          = {Cambridge University Press},
        TITLE              = {Inductive sets and families in {Martin-L{\"o}f's}
 Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, 
        VOLUME             = {14},
        YEAR               = {1991}
}

@ARTICLE{Dyc92,
        AUTHOR             = {Roy Dyckhoff},
        JOURNAL            = {The Journal of Symbolic Logic},
        MONTH              = sep,
        NUMBER             = {3},
        TITLE              = {Contraction-free sequent calculi for intuitionistic logic},
        VOLUME             = {57},
        YEAR               = {1992}
}

@MASTERSTHESIS{Fil94,
        AUTHOR             = {J.-C. Filli\^atre},
        MONTH              = sep,
        SCHOOL             = {DEA d'Informatique, ENS Lyon},
        TITLE              = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. {\'E}tude et impl\'ementation dans le syst\`eme {\Coq}},
        YEAR               = {1994}
}

@TECHREPORT{Filliatre95,
        AUTHOR             = {J.-C. Filli\^atre},
        INSTITUTION        = {LIP-ENS-Lyon},
        TITLE              = {A decision procedure for Direct Predicate Calculus},
        TYPE               = {Research report},
        NUMBER             = {96--25},
        YEAR               = {1995}
}

@Article{Filliatre03jfp,
  author = 	 {J.-C. Filli{\^a}tre},
  title = 	 {Verification of Non-Functional Programs 
                   using Interpretations in Type Theory},
  journal =      jfp,
  volume =       13,
  number =       4,
  pages =        {709--745},
  month =	 jul,
  year =	 2003,
  note = 	 {[English translation of \cite{Filliatre99}]},
  url =          {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz},
  topics =       "team, lri",
  type_publi =   "irevcomlec"
}


@PhdThesis{Filliatre99,
  author = 	 {J.-C. Filli\^atre},
  title = 	 {Preuve de programmes imp\'eratifs en th\'eorie des types},
  type =         {Th{\`e}se de Doctorat},
  school = 	 {Universit\'e Paris-Sud},
  year = 	 1999,
  month =	 {July},
  url =         {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}}
}

@Unpublished{Filliatre99c,
  author = 	 {J.-C. Filli\^atre},
  title = 	 {{Formal Proof of a Program: Find}},
  month =        {January},
  year =         2000,
  note = 	 {Submitted to \emph{Science of Computer Programming}},
  url =         {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}}
}

@InProceedings{FilliatreMagaud99,
  author = 	 {J.-C. Filli\^atre and N. Magaud},
  title = 	 {Certification of sorting algorithms in the system {\Coq}},
  booktitle =    {Theorem Proving in Higher Order Logics: 
                  Emerging Trends},
  year =	 1999,
  url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}}
}

@UNPUBLISHED{Fle90,
        AUTHOR             = {E. Fleury},
        MONTH              = jul,
        NOTE               = {Rapport de Stage},
        TITLE              = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}},
        YEAR               = {1990}
}

@BOOK{Fourier,
        AUTHOR             = {Jean-Baptiste-Joseph Fourier},
        PUBLISHER          = {Gauthier-Villars},
        TITLE              = {Fourier's method to solve linear 
                              inequations/equations systems.},
        YEAR               = {1890}
}

@INPROCEEDINGS{Gim94,
        AUTHOR             = {E. Gim\'enez},
        BOOKTITLE          = {Types'94 : Types for Proofs and Programs},
        NOTE               = {Extended version in LIP research report 95-07, ENS Lyon},
        PUBLISHER          = SV,
        SERIES             = LNCS,
        TITLE              = {Codifying guarded definitions with recursive schemes},
        VOLUME             = {996},
        YEAR               = {1994}
}

@TECHREPORT{Gim98,
  AUTHOR       = {E. Gim\'enez},
  TITLE        = {A Tutorial on Recursive Types in Coq},
  INSTITUTION  = {INRIA},
  YEAR         = 1998,
  MONTH        = mar
}

@UNPUBLISHED{GimCas05,
  AUTHOR       = {E. Gim\'enez and P. Cast\'eran},
  TITLE        = {A Tutorial on [Co-]Inductive Types in Coq},
  INSTITUTION  = {INRIA},
  YEAR         = 2005,
  MONTH        = jan,
  NOTE         = {available at \url{http://coq.inria.fr/doc}}
} 

@INPROCEEDINGS{Gimenez95b,
        AUTHOR             = {E. Gim\'enez},
        BOOKTITLE          = {Workshop on Types for Proofs and Programs},
        SERIES             = LNCS,
        NUMBER             = {1158},
        PAGES              = {135-152},
        TITLE              = {An application of co-Inductive types in Coq: 
		               verification of the Alternating Bit Protocol},
        EDITORS            = {S. Berardi and M. Coppo},
        PUBLISHER          = SV,
        YEAR               = {1995}
}

@INPROCEEDINGS{Gir70,
        AUTHOR             = {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              = {{\'E}criture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
        YEAR               = {1994}
}

@INPROCEEDINGS{HofStr98,
        AUTHOR        = {Martin Hofmann and Thomas Streicher},
        TITLE         = {The groupoid interpretation of type theory},
        BOOKTITLE     = {Proceedings of the meeting Twenty-five years of constructive type theory},
        PUBLISHER     = {Oxford University Press},
        YEAR          = {1998}
} 

@INCOLLECTION{How80,
        AUTHOR             = {W.A. Howard},
        BOOKTITLE          = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
        EDITOR             = {J.P. Seldin and J.R. Hindley},
        NOTE               = {Unpublished 1969 Manuscript},
        PUBLISHER          = {Academic Press},
        TITLE              = {The Formulae-as-Types Notion of Constructions},
        YEAR               = {1980}
}

@InProceedings{Hue87tapsoft,
  author = 	 {G. Huet},
  title = 	 {Programming of Future Generation Computers},
  booktitle = 	 {Proceedings of TAPSOFT87},
       series = LNCS,
        volume = 249,
  pages =	 {276--286},
  year =	 1987,
  publisher =	 SV
}

@INPROCEEDINGS{Hue87,
        AUTHOR             = {G. Huet},
        BOOKTITLE          = {Programming of Future Generation Computers},
        EDITOR             = {K. Fuchi and M. Nivat},
        NOTE               = {Also in \cite{Hue87tapsoft}},
        PUBLISHER          = {Elsevier Science},
        TITLE              = {Induction Principles Formalized in the {Calculus of Constructions}},
        YEAR               = {1988}
}

@INPROCEEDINGS{Hue88,
        AUTHOR             = {G. Huet},
        BOOKTITLE          = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
        EDITOR             = {R. Narasimhan},
        NOTE               = {Also in~\cite{CoC89}},
        PUBLISHER          = {World Scientific Publishing},
        TITLE              = {{The Constructive Engine}},
        YEAR               = {1989}
}

@BOOK{Hue89,
        EDITOR             = {G. Huet},
        PUBLISHER          = {Addison-Wesley},
        SERIES             = {The UT Year of Programming Series},
        TITLE              = {Logical Foundations of Functional Programming},
        YEAR               = {1989}
}

@INPROCEEDINGS{Hue92,
        AUTHOR             = {G. Huet},
        BOOKTITLE          = {Proceedings of 12th FST/TCS Conference, New Delhi},
        PAGES              = {229--240},
        PUBLISHER          = SV,
        SERIES             = LNCS,
        TITLE              = {The Gallina Specification Language : A case study},
        VOLUME             = {652},
        YEAR               = {1992}
}

@ARTICLE{Hue94,
        AUTHOR             = {G. Huet},
        JOURNAL            = {J. Functional Programming},
        PAGES              = {371--394},
        PUBLISHER          = {Cambridge University Press},
        TITLE              = {Residual theory in $\lambda$-calculus: a formal development},
        VOLUME             = {4,3},
        YEAR               = {1994}
}

@INCOLLECTION{HuetLevy79,
        AUTHOR             = {G. Huet and J.-J. L\'{e}vy},
        TITLE              = {Call by Need Computations in Non-Ambigous
Linear Term Rewriting Systems},
        NOTE               = {Also research report 359, INRIA, 1979},
        BOOKTITLE          = {Computational Logic, Essays in Honor of
Alan Robinson},
        EDITOR             = {J.-L. Lassez and G. Plotkin},
        PUBLISHER          = {The MIT press},
        YEAR               = {1991}
}

@ARTICLE{KeWe84,
        AUTHOR             = {J. Ketonen and R. Weyhrauch},
        JOURNAL            = {Theoretical Computer Science},
        PAGES              = {297--307},
        TITLE              = {A decidable fragment of {P}redicate {C}alculus},
        VOLUME             = {32},
        YEAR               = {1984}
}

@BOOK{Kle52,
        AUTHOR             = {S.C. Kleene},
        PUBLISHER          = {North-Holland},
        SERIES             = {Bibliotheca Mathematica},
        TITLE              = {Introduction to Metamathematics},
        YEAR               = {1952}
}

@BOOK{Kri90,
        AUTHOR             = {J.-L. Krivine},
        PUBLISHER          = {Masson},
        SERIES             = {Etudes et recherche en informatique},
        TITLE              = {Lambda-calcul {types et mod\`eles}},
        YEAR               = {1990}
}

@BOOK{LE92,
        EDITOR             = {G. Huet and G. Plotkin},
        PUBLISHER          = {Cambridge University Press},
        TITLE              = {Logical Environments},
        YEAR               = {1992}
}

@BOOK{LF91,
        EDITOR             = {G. Huet and G. Plotkin},
        PUBLISHER          = {Cambridge University Press},
        TITLE              = {Logical Frameworks},
        YEAR               = {1991}
}

@ARTICLE{Laville91,
        AUTHOR             = {A. Laville},
        TITLE              = {Comparison of Priority Rules in Pattern
Matching and Term Rewriting},
        JOURNAL            = {Journal of Symbolic Computation},
        VOLUME             = {11},
        PAGES              = {321--347},
        YEAR               = {1991}
}

@INPROCEEDINGS{LePa94,
        AUTHOR             = {F. Leclerc and C. Paulin-Mohring},
        BOOKTITLE          = {{Types for Proofs and Programs, Types' 93}},
        EDITOR             = {H. Barendregt and T. Nipkow},
        PUBLISHER          = SV,
        SERIES             = {LNCS},
        TITLE              = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}},
        VOLUME             = {806},
        YEAR               = {1994}
}

@TECHREPORT{Leroy90,
        AUTHOR             = {X. Leroy},
        TITLE              = {The {ZINC} experiment: an economical implementation
of the {ML} language},
        INSTITUTION        = {INRIA},
        NUMBER             = {117},
        YEAR               = {1990}
}

@INPROCEEDINGS{Let02,
        author          = {P. Letouzey},
        title           = {A New Extraction for Coq},
        booktitle       = {Proceedings of the TYPES'2002 workshop},
        year            = 2002,
        note            = {to appear},
        url            = {draft at \url{http://www.lri.fr/~letouzey/download/extraction2002.ps.gz}}
}

@PHDTHESIS{Luo90,
        AUTHOR             = {Z. Luo},
        TITLE              = {An Extended Calculus of Constructions},
        SCHOOL             = {University of Edinburgh},
        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{Miquel00,
        AUTHOR             = {A. Miquel},
        TITLE              = {A Model for Impredicative Type Systems with Universes,
Intersection Types and Subtyping},
        BOOKTITLE          = {{Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00)}},
        PUBLISHER          = {IEEE Computer Society Press},
        YEAR               = {2000}
}

@PHDTHESIS{Miquel01a,
        AUTHOR             = {A. Miquel},
        TITLE              = {Le Calcul des Constructions implicite: syntaxe et s\'emantique},
        MONTH              = {dec},
        SCHOOL             = {{Universit\'e Paris 7}},
        YEAR               = {2001}
}

@INPROCEEDINGS{Miquel01b,
        AUTHOR             = {A. Miquel},
        TITLE              = {The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping},
        BOOKTITLE          = {{Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA01), Krakow, Poland}},
        PUBLISHER          = SV,
        SERIES             = {LNCS},
        NUMBER             = 2044,
        YEAR               = {2001}
}

@INPROCEEDINGS{MiWer02,
        AUTHOR             = {A. Miquel and B. Werner},
        TITLE              = {The Not So Simple Proof-Irrelevant Model of CC},
        BOOKTITLE          = {Types for Proofs and Programs (TYPES'02)},
        PUBLISHER          = SV,
        SERIES             = {LNCS},
        NUMBER             = 2646,
        YEAR               = 2003
}


@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          = SV,
        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{NoPS90,
        AUTHOR             = {B. {Nordstr\"om} and K. Peterson and J. Smith},
        BOOKTITLE          = {Information Processing 83},
        PUBLISHER          = {Oxford Science Publications},
        SERIES             = {International Series of Monographs on Computer Science},
        TITLE              = {Programming in {Martin-L\"of's} Type Theory},
        YEAR               = {1990}
}

@ARTICLE{Nor88,
        AUTHOR             = {B. {Nordstr\"om}},
        JOURNAL            = {BIT},
        TITLE              = {Terminating General Recursion},
        VOLUME             = {28},
        YEAR               = {1988}
}

@BOOK{Odi90,
        EDITOR             = {P. Odifreddi},
        PUBLISHER          = {Academic Press},
        TITLE              = {Logic and Computer Science},
        YEAR               = {1990}
}

@INPROCEEDINGS{PaMS92,
        AUTHOR             = {M. Parigot and P. Manoury and M. Simonot},
        ADDRESS            = {St. Petersburg, Russia},
        BOOKTITLE          = {Logic Programming and automated reasoning},
        EDITOR             = {A. Voronkov},
        MONTH              = jul,
        NUMBER             = {624},
        PUBLISHER          = SV,
        SERIES             = {LNCS},
        TITLE              = {{ProPre : A Programming language with proofs}},
        YEAR               = {1992}
}

@ARTICLE{PaWe92,
        AUTHOR             = {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          = SV,
        SERIES             = {LNCS},
        TITLE              = {{Synthesizing proofs from programs in
the Calculus of Inductive Constructions}},
        VOLUME             = {947},
        YEAR               = {1995}
}

@INPROCEEDINGS{Prasad93,
        AUTHOR             = {K.V. Prasad},
        BOOKTITLE          = {{Proceedings of CONCUR'93}},
        PUBLISHER          = SV,
        SERIES             = {LNCS},
        TITLE              = {{Programming with broadcasts}},
        VOLUME             = {715},
        YEAR               = {1993}
}

@BOOK{RC95,
  author = "di~Cosmo, R.",
  title  = "Isomorphisms of Types: from $\lambda$-calculus to information
            retrieval and language design",
  series = "Progress in Theoretical Computer Science",
  publisher = "Birkhauser",
  year = "1995",
  note = "ISBN-0-8176-3763-X"
}

@TECHREPORT{Rou92,
        AUTHOR             = {J. Rouyer},
        INSTITUTION        = {INRIA},
        MONTH              = nov,
        NUMBER             = {1795},
        TITLE              = {{D{\'e}veloppement de l'Algorithme d'Unification dans le Calcul des Constructions}},
        YEAR               = {1992}
}

@article{Rushby98,
	TITLE = {Subtypes for Specifications: Predicate Subtyping in
		{PVS}},
	AUTHOR = {John Rushby and Sam Owre and N. Shankar},
	JOURNAL = {IEEE Transactions on Software Engineering},
	PAGES = {709--720},
	VOLUME = 24,
	NUMBER = 9,
	MONTH = sep,
	YEAR = 1998
}

@TECHREPORT{Saibi94,
        AUTHOR             = {A. Sa\"{\i}bi},
        INSTITUTION        = {INRIA},
        MONTH              = dec,
        NUMBER             = {2345},
        TITLE              = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}},
        YEAR               = {1994}
}


@MASTERSTHESIS{Ter92,
        AUTHOR             = {D. Terrasse},
        MONTH              = sep,
        SCHOOL             = {IARFA},
        TITLE              = {{Traduction de TYPOL en COQ. Application \`a Mini ML}},
        YEAR               = {1992}
}

@TECHREPORT{ThBeKa92,
        AUTHOR             = {L. Th\'ery and Y. Bertot and G. Kahn},
        INSTITUTION        = {INRIA Sophia},
        MONTH              = may,
        NUMBER             = {1684},
        TITLE              = {Real theorem provers deserve real user-interfaces},
        TYPE               = {Research Report},
        YEAR               = {1992}
}

@BOOK{TrDa89,
        AUTHOR             = {A.S. Troelstra and D. van Dalen},
        PUBLISHER          = {North-Holland},
        SERIES             = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123},
        TITLE              = {Constructivism in Mathematics, an introduction},
        YEAR               = {1988}
}

@PHDTHESIS{Wer94,
        AUTHOR             = {B. Werner},
        SCHOOL             = {Universit\'e Paris 7},
        TITLE              = {Une th\'eorie des constructions inductives},
        TYPE               = {Th\`ese de Doctorat},
        YEAR               = {1994}
}

@PHDTHESIS{Bar99,
        AUTHOR             = {B. Barras},
        SCHOOL             = {Universit\'e Paris 7},
        TITLE              = {Auto-validation d'un système de preuves avec familles inductives},
        TYPE               = {Th\`ese de Doctorat},
        YEAR               = {1999}
}

@UNPUBLISHED{ddr98,
	AUTHOR	           = {D. de Rauglaudre},
        TITLE              = {Camlp4 version 1.07.2},
        YEAR               = {1998},
        NOTE               = {In Camlp4 distribution}
}

@ARTICLE{dowek93,
        AUTHOR             = {G. Dowek},
        TITLE              = {{A Complete Proof Synthesis Method for the Cube of Type Systems}},
        JOURNAL            = {Journal Logic Computation},
        VOLUME             = {3},
        NUMBER             = {3},
        PAGES              = {287--315},
        MONTH              = {June},
        YEAR               = {1993}
}

@INPROCEEDINGS{manoury94,
        AUTHOR             = {P. Manoury},
        TITLE              = {{A User's Friendly Syntax to Define
Recursive Functions as Typed $\lambda-$Terms}},
        BOOKTITLE          = {{Types for Proofs and Programs, TYPES'94}},
        SERIES             = {LNCS},
        VOLUME             = {996},
        MONTH              = jun,
        YEAR               = {1994}
}

@TECHREPORT{maranget94,
        AUTHOR             = {L. Maranget},
        INSTITUTION        = {INRIA},
        NUMBER             = {2385},
        TITLE              = {{Two Techniques for Compiling Lazy Pattern Matching}},
        YEAR               = {1994}
}

@INPROCEEDINGS{puel-suarez90,
        AUTHOR             = {L.Puel and A. Su\'arez},
        BOOKTITLE          = {{Conference Lisp and Functional Programming}},
        SERIES             = {ACM},
        PUBLISHER          = SV,
        TITLE              = {{Compiling Pattern Matching by Term
Decomposition}},
        YEAR               = {1990}
}

@MASTERSTHESIS{saidi94,
        AUTHOR             = {H. Saidi},
        MONTH              = sep,
        SCHOOL             = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
        TITLE              = {R\'esolution d'\'equations dans le syst\`eme T
 de G\"odel},
        YEAR               = {1994}
}

@misc{streicher93semantical,
  author = "T. Streicher",
  title = "Semantical Investigations into Intensional Type Theory",
  note = "Habilitationsschrift, LMU Munchen.",
  year = "1993" }



@Misc{Pcoq,
  author =	 {Lemme Team},
  title =	 {Pcoq a graphical user-interface for {Coq}},
  note =	 {\url{http://www-sop.inria.fr/lemme/pcoq/}}
}


@Misc{ProofGeneral,
  author =	 {David Aspinall},
  title =	 {Proof General},
  note =	 {\url{http://proofgeneral.inf.ed.ac.uk/}}
}

@Book{CoqArt,
   title = "Interactive Theorem Proving and Program Development.
    Coq'Art: The Calculus of Inductive Constructions",
   author = "Yves Bertot and Pierre Castéran",
   publisher = "Springer Verlag",
   series = "Texts in Theoretical Computer Science. An EATCS series", 
 year = 2004
  }



@INCOLLECTION{wadler87,
        AUTHOR             = {P. Wadler},
        TITLE              = {Efficient  Compilation of Pattern Matching},
        BOOKTITLE          = {The Implementation of Functional Programming
Languages},
        EDITOR             = {S.L. Peyton Jones},
        PUBLISHER          = {Prentice-Hall},
        YEAR               = {1987}
}


@COMMENT{cross-references, must be at end}

@BOOK{Bastad92,
        EDITOR             = {B. Nordstr\"om and K. Petersson and G. Plotkin},
        PUBLISHER          = {Available by ftp at site ftp.inria.fr},
        TITLE              = {Proceedings of the 1992 Workshop on Types for Proofs and Programs},
        YEAR               = {1992}
}

@BOOK{Nijmegen93,
        EDITOR             = {H. Barendregt and T. Nipkow},
        PUBLISHER          = SV,
        SERIES             = LNCS,
        TITLE              = {Types for Proofs and Programs},
        VOLUME             = {806},
        YEAR               = {1994}
}