Merge PR #7467: Remove unused references from biblio.

1 files changed, 88 insertions, 1066 deletions

diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index aeb45611e..3e988709c 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -3,47 +3,6 @@
 @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},
@@ -51,55 +10,6 @@ Computer Architecture},
   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},
@@ -112,15 +22,6 @@ s},
   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.},
@@ -129,121 +30,6 @@ s},
   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,
@@ -261,24 +47,6 @@ s},
   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}},
@@ -286,49 +54,18 @@ s},
   booktitle   = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}
 }
 
-@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}
+@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}
 }
 
-@book{Cur58,
+@Book{Cur58,
   author      = {Haskell B. Curry and Robert Feys and William Craig},
   title       = {Combinatory Logic},
   volume      = 1,
@@ -337,17 +74,40 @@ s},
   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}"
+@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{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},
 }
 
 @InProceedings{Del00,
@@ -361,99 +121,7 @@ s},
   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     = {Theoretical Computer Science},
-  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}
+  url         = {http://www.lirmm.fr/\%7Edelahaye/papers/ltac\%20(LPAR\%2700).pdf}
 }
 
 @Article{Dyc92,
@@ -466,75 +134,6 @@ s},
   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},
@@ -554,13 +153,6 @@ s},
   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},
@@ -591,21 +183,6 @@ s},
   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},
@@ -614,32 +191,6 @@ s},
   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.},
@@ -650,27 +201,6 @@ s},
   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},
@@ -680,112 +210,17 @@ s},
   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}
+@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}
 }
 
 @TechReport{Leroy90,
@@ -805,14 +240,7 @@ Matching and Term Rewriting},
   url         = {draft at \url{http://www.irif.fr/~letouzey/download/extraction2002.pdf}}
 }
 
-@PhDThesis{Luo90,
-  author      = {Z. Luo},
-  title       = {An Extended Calculus of Constructions},
-  school      = {University of Edinburgh},
-  year        = {1990}
-}
-
-@inproceedings{Luttik97specificationof,
+@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},
@@ -820,92 +248,15 @@ Matching and Term Rewriting},
   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{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}
 }
 
 @InProceedings{Moh93,
@@ -920,14 +271,6 @@ Intersection Types and Subtyping},
   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,
@@ -936,73 +279,6 @@ Intersection Types and Subtyping},
   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}},
@@ -1014,14 +290,16 @@ the Calculus of Inductive Constructions}},
   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}
+@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{RC95,
@@ -1034,15 +312,6 @@ the Calculus of Inductive Constructions}},
   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}},
@@ -1055,115 +324,7 @@ the Calculus of Inductive Constructions}},
   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,
+@InProceedings{sozeau06,
   author = {Matthieu Sozeau},
   title = {Subset Coercions in {C}oq},
   year = {2007},
@@ -1174,7 +335,7 @@ Decomposition}},
   series =    {LNCS}
 }
 
-@inproceedings{sozeau08,
+@InProceedings{sozeau08,
         Author = {Matthieu Sozeau and Nicolas Oury},
         booktitle = {TPHOLs'08},
         Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf},
@@ -1182,87 +343,7 @@ Decomposition}},
         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/}}
-}
-
-@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,
+@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},
@@ -1271,38 +352,7 @@ Languages},
     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,
+@Article{TheOmegaPaper,
     author = "W. Pugh",
     title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis",
     journal = "Communication of the ACM",
@@ -1310,43 +360,15 @@ Languages},
     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},
+@PhDThesis{Wer94,
+  author      = {B. Werner},
+  school      = {Universit\'e Paris 7},
+  title       = {Une th\'eorie des constructions inductives},
+  type        = {Th\`ese de Doctorat},
+  year        = {1994}
 }
 
-@inproceedings{CompiledStrongReduction,
+@InProceedings{CompiledStrongReduction,
   author    = {Benjamin Gr{\'{e}}goire and
                Xavier Leroy},
   editor    = {Mitchell Wand and
@@ -1365,7 +387,7 @@ Languages},
   bibsource = {dblp computer science bibliography, http://dblp.org}
 }
 
-@inproceedings{FullReduction,
+@InProceedings{FullReduction,
   author    = {Mathieu Boespflug and
                Maxime D{\'{e}}n{\`{e}}s and
                Benjamin Gr{\'{e}}goire},