@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       = {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},
  title       = {Mathematical Quotients and Quotient Types in Coq},
  booktitle   = {TYPES},
  crossref    = {DBLP:conf/types/2002},
  year        = {2002}
}

@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},
  booktitle   = {Types for Proofs and Programs},
  editor      = {H. Barendregt and T. Nipokow},
  publisher   = SV,
  series      = LNCS,
  title       = {{Infinite objects in Type Theory}},
  volume      = {806},
  year        = {1993},
  pages       = {62-78}
}

@inproceedings{Corbineau08types,
  author      = {P. Corbineau},
  title       = {A Declarative Language for the Coq Proof Assistant},
  editor      = {M. Miculan and I. Scagnetto and F. Honsell},
  booktitle   = {TYPES '07, Cividale del Friuli, Revised Selected Papers},
  publisher   = {Springer},
  series      = LNCS,
  volume      = {4941},
  year        = {2007},
  pages       = {69-84},
  ee          = {http://dx.doi.org/10.1007/978-3-540-68103-8_5},
}

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

@book{Cur58,
  author      = {Haskell B. Curry and Robert Feys and William Craig},
  title       = {Combinatory Logic},
  volume      = 1, 
  publisher   = "North-Holland",
  year        = 1958,
  note        = {{\S{9E}}},
}

@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ö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. É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â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è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}
}

@PhDThesis{Gim96,
  author      = {E. Gim\'enez},
  title       = {Un calcul des constructions infinies et son application \'a la v\'erification de syst\`emes communicants},
  school      = {\'Ecole Normale Sup\'erieure de Lyon},
  year        = {1996}
}

@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       = {É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}
}

@Unpublished{Hue88b,
  author      = {G. Huet},
  title       = {Extending the Calculus of Constructions with Type:Type},
  year        = 1988,
  note        = {Unpublished}
}

@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   = {TYPES},
  year        = 2002,
  crossref    = {DBLP:conf/types/2002},
  url         = {draft at \url{http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz}}
}

@PhDThesis{Luo90,
  author      = {Z. Luo},
  title       = {An Extended Calculus of Constructions},
  school      = {University of Edinburgh},
  year        = {1990}
}

@inproceedings{Luttik97specificationof,
	Author = {Sebastiaan P. Luttik and Eelco Visser},
	Booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing},
	Publisher = {Springer-Verlag},
	Title = {Specification of Rewriting Strategies},
	Year = {1997}}

@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},
  title       = {Automatizing Termination Proofs of Recursively Defined Functions.},
  journal     = {TCS},
  volume      = {135},
  number      = {2},
  year        = {1994},
  pages       = {319-343},
}

@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},
  year        = {2002},
  pages       = {240-258},
  ee          = {http://link.springer.de/link/service/series/0558/bibs/2646/26460240.htm},
  crossref    = {DBLP:conf/types/2002},
  bibsource   = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/types/2002,
  editor      = {H. Geuvers and F. Wiedijk},
  title       = {Types for Proofs and Programs, Second International Workshop,
                 TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002,
                 Selected Papers},
  booktitle   = {TYPES},
  publisher   = SV,
  series      = LNCS,
  volume      = {2646},
  year        = {2003},
  isbn        = {3-540-14031-X},
  bibsource   = {DBLP, http://dblp.uni-trier.de}
}

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

@inproceedings{sozeau06,
  author = {Matthieu Sozeau},
  title = {Subset Coercions in {C}oq},
  year = {2007},
  booktitle = {TYPES'06},
  pages = {237-252},
  volume = {4502},
  publisher = "Springer",
  series =    {LNCS}
}

@inproceedings{sozeau08,
	Author = {Matthieu Sozeau and Nicolas Oury},
	booktitle = {TPHOLs'08},
	Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf},
	Title = {{F}irst-{C}lass {T}ype {C}lasses},
	Year = {2008},
}

@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{https://proofgeneral.github.io/}}
}

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

@inproceedings{DBLP:conf/types/CornesT95,
  author    = {Cristina Cornes and
               Delphine Terrasse},
  title     = {Automating Inversion of Inductive Predicates in Coq},
  booktitle = {TYPES},
  year      = {1995},
  pages     = {85-104},
  crossref  = {DBLP:conf/types/1995},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/types/1995,
  editor    = {Stefano Berardi and
               Mario Coppo},
  title     = {Types for Proofs and Programs, International Workshop TYPES'95,
               Torino, Italy, June 5-8, 1995, Selected Papers},
  booktitle = {TYPES},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1158},
  year      = {1996},
  isbn      = {3-540-61780-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/types/McBride00,
  author    = {Conor McBride},
  title     = {Elimination with a Motive},
  booktitle = {TYPES},
  year      = {2000},
  pages     = {197-216},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm},
  crossref  = {DBLP:conf/types/2000},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/types/2000,
  editor    = {Paul Callaghan and
               Zhaohui Luo and
               James McKinna and
               Robert Pollack},
  title     = {Types for Proofs and Programs, International Workshop, TYPES
               2000, Durham, UK, December 8-12, 2000, Selected Papers},
  booktitle = {TYPES},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2277},
  year      = {2002},
  isbn      = {3-540-43287-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{sugar,
    author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso},
    title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm},
    booktitle = { Proceedings of the ISSAC'91, ACM Press},
    year = {1991},
    pages = {5--4},
    publisher = {}
}

@article{LeeWerner11,
  author    = {Gyesik Lee and
               Benjamin Werner},
  title     = {Proof-irrelevant model of {CC} with predicative induction
               and judgmental equality},
  journal   = {Logical Methods in Computer Science},
  volume    = {7},
  number    = {4},
  year      = {2011},
  ee        = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

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

@article{ TheOmegaPaper,
    author = "W. Pugh",
    title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis",
    journal = "Communication of the ACM",
    pages = "102--114",
    year = "1992",
}

@inproceedings{CSwcu,
    hal_id = {hal-00816703},
    url = {http://hal.inria.fr/hal-00816703},
    title = {{Canonical Structures for the working Coq user}},
    author = {Mahboubi, Assia and Tassi, Enrico},
    booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}},
    publisher = {Springer},
    pages = {19-34},
    address = {Rennes, France},
    volume = {7998},
    editor = {Sandrine Blazy and Christine Paulin and David Pichardie },
    series = {LNCS },
    doi = {10.1007/978-3-642-39634-2\_5 },
    year = {2013},
}

@article{CSlessadhoc,
 author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek},
 title = {How to Make Ad Hoc Proof Automation Less Ad Hoc},
 journal = {SIGPLAN Not.},
 issue_date = {September 2011},
 volume = {46},
 number = {9},
 month = sep,
 year = {2011},
 issn = {0362-1340},
 pages = {163--175},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/2034574.2034798},
 doi = {10.1145/2034574.2034798},
 acmid = {2034798},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes},
}

@inproceedings{CompiledStrongReduction,
  author    = {Benjamin Gr{\'{e}}goire and
               Xavier Leroy},
  editor    = {Mitchell Wand and
               Simon L. Peyton Jones},
  title     = {A compiled implementation of strong reduction},
  booktitle = {Proceedings of the Seventh {ACM} {SIGPLAN} International Conference
               on Functional Programming {(ICFP} '02), Pittsburgh, Pennsylvania,
               USA, October 4-6, 2002.},
  pages     = {235--246},
  publisher = {{ACM}},
  year      = {2002},
  url       = {http://doi.acm.org/10.1145/581478.581501},
  doi       = {10.1145/581478.581501},
  timestamp = {Tue, 11 Jun 2013 13:49:16 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/icfp/GregoireL02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{FullReduction,
  author    = {Mathieu Boespflug and
               Maxime D{\'{e}}n{\`{e}}s and
               Benjamin Gr{\'{e}}goire},
  editor    = {Jean{-}Pierre Jouannaud and
               Zhong Shao},
  title     = {Full Reduction at Full Throttle},
  booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
               2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7086},
  pages     = {362--377},
  publisher = {Springer},
  year      = {2011},
  url       = {http://dx.doi.org/10.1007/978-3-642-25379-9_26},
  doi       = {10.1007/978-3-642-25379-9_26},
  timestamp = {Thu, 17 Nov 2011 13:33:48 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}