[Sphinx] add bibliography

3 files changed, 1407 insertions, 1 deletions

diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
new file mode 100644
index 000000000..4a9bd6c1a
--- /dev/null
+++ b/doc/sphinx/biblio.bib
@@ -0,0 +1,1397 @@
+@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},
+  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}
+}
+
+@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     = {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}
+}
+
+@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.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,
+        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}
+}
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 4a3548c1d..ef2fdc06e 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -19,7 +19,8 @@ Table of contents
 
 .. toctree::
    :caption: Reference
-   :titlesonly:
+
+   zebibliography
 
 .. toctree::
    :caption: Indexes
diff --git a/doc/sphinx/zebibliography.rst b/doc/sphinx/zebibliography.rst
new file mode 100644
index 000000000..0000caa30
--- /dev/null
+++ b/doc/sphinx/zebibliography.rst
@@ -0,0 +1,8 @@
+.. _bibliography:
+
+============
+Bibliography
+============
+
+.. bibliography:: biblio.bib
+   :cited: