merge faq hugo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8557 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 1782 insertions, 7 deletions

diff --git a/doc/newfaq/fk.bib b/doc/newfaq/fk.bib
index 77baf97998..594de63484 100644
--- a/doc/newfaq/fk.bib
+++ b/doc/newfaq/fk.bib
@@ -1130,3 +1130,1094 @@ cedures.},
   year =         {2004},
   url =          "http://coq.inria.fr"
 }
+
+@string{jfp = "Journal of Functional Programming"}
+@STRING{lncs="Lecture Notes in Computer Science"}
+@STRING{lnai="Lecture Notes in Artificial Intelligence"}
+@string{SV = "{Sprin\-ger-Verlag}"}
+
+@INPROCEEDINGS{Aud91,
+        AUTHOR             = {Ph. Audebaud},
+        BOOKTITLE          = {Proceedings of the sixth Conf. on Logic in Computer Science.},
+        PUBLISHER          = {IEEE},
+        TITLE              = {Partial {Objects} in the {Calculus of Constructions}},
+        YEAR               = {1991}
+}
+
+@PHDTHESIS{Aud92,
+        AUTHOR             = {Ph. Audebaud},
+        SCHOOL             = {{Universit\'e} Bordeaux I},
+        TITLE              = {Extension du Calcul des Constructions par Points fixes},
+        YEAR               = {1992}
+}
+
+@INPROCEEDINGS{Audebaud92b,
+        AUTHOR             = {Ph. Audebaud},
+        BOOKTITLE          = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}},
+        EDITOR             = {{B. Nordstr\"om and K. Petersson and G. Plotkin}},
+        NOTE               = {Also Research Report LIP-ENS-Lyon},
+        PAGES              = {pp 21--34},
+        TITLE              = {{CC+ : an extension of the Calculus of Constructions with fixpoints}},
+        YEAR               = {1992}
+}
+
+@INPROCEEDINGS{Augustsson85,
+        AUTHOR             = {L. Augustsson},
+        TITLE              = {{Compiling Pattern Matching}},
+        BOOKTITLE          = {Conference Functional Programming and
+Computer Architecture},
+        YEAR               = {1985}
+}
+
+@ARTICLE{BaCo85,
+        AUTHOR             = {J.L. Bates and R.L. Constable},
+        JOURNAL            = {ACM transactions on Programming Languages and Systems},
+        TITLE              = {Proofs as {Programs}},
+        VOLUME             = {7},
+        YEAR               = {1985}
+}
+
+@BOOK{Bar81,
+        AUTHOR             = {H.P. Barendregt},
+        PUBLISHER          = {North-Holland},
+        TITLE              = {The Lambda Calculus its Syntax and Semantics},
+        YEAR               = {1981}
+}
+
+@TECHREPORT{Bar91,
+        AUTHOR             = {H. Barendregt},
+        INSTITUTION        = {Catholic University Nijmegen},
+        NOTE               = {In Handbook of Logic in Computer Science, Vol II},
+        NUMBER             = {91-19},
+        TITLE              = {Lambda {Calculi with Types}},
+        YEAR               = {1991}
+}
+
+@ARTICLE{BeKe92,
+        AUTHOR             = {G. Bellin and J. Ketonen},
+        JOURNAL            = {Theoretical Computer Science},
+        PAGES              = {115--142},
+        TITLE              = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation},
+        VOLUME             = {95},
+        YEAR               = {1992}
+}
+
+@BOOK{Bee85,
+        AUTHOR             = {M.J. Beeson},
+        PUBLISHER          = SV,
+        TITLE              = {Foundations of Constructive Mathematics, Metamathematical Studies},
+        YEAR               = {1985}
+}
+
+@BOOK{Bis67,
+        AUTHOR             = {E. Bishop},
+        PUBLISHER          = {McGraw-Hill},
+        TITLE              = {Foundations of Constructive Analysis},
+        YEAR               = {1967}
+}
+
+@BOOK{BoMo79,
+        AUTHOR             = {R.S. Boyer and J.S. Moore},
+        KEY                = {BoMo79},
+        PUBLISHER          = {Academic Press},
+        SERIES             = {ACM Monograph},
+        TITLE              = {A computational logic},
+        YEAR               = {1979}
+}
+
+@MASTERSTHESIS{Bou92,
+        AUTHOR             = {S. Boutin},
+        MONTH              = sep,
+        SCHOOL             = {{Universit\'e Paris 7}},
+        TITLE              = {Certification d'un compilateur {ML en Coq}},
+        YEAR               = {1992}
+}
+
+@inproceedings{Bou97,
+   title = {Using reflection to build efficient and certified decision procedure
+s},
+   author = {S. Boutin},
+   booktitle = {TACS'97},
+   editor = {Martin Abadi and Takahashi Ito},
+   publisher = SV,
+   series = lncs,
+   volume=1281, 
+   PS={http://pauillac.inria.fr/~boutin/public_w/submitTACS97.ps.gz}, 
+   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{CPar93,
+        AUTHOR             = {C. Parent},
+        INSTITUTION        = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
+        MONTH              = oct,
+        NOTE               = {Also in~\cite{Nijmegen93}},
+        NUMBER             = {93-29},
+        TITLE              = {Developing certified programs in the system {Coq}- {The} {Program} tactic},
+        YEAR               = {1993}
+}
+
+@PHDTHESIS{CPar95,
+        AUTHOR             = {C. Parent},
+        SCHOOL             = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
+        TITLE              = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}},
+        YEAR               = {1995}
+}
+
+@BOOK{Caml,
+        AUTHOR             = {P. Weis and X. Leroy},
+        PUBLISHER          = {InterEditions},
+        TITLE              = {Le langage Caml},
+        YEAR               = {1993}
+}
+
+@INPROCEEDINGS{ChiPotSimp03,
+  AUTHOR    = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson},
+  ADDRESS   = {Berg en Dal, The Netherlands},
+  TITLE     = {Mathematical Quotients and Quotient Types in Coq},
+  BOOKTITLE = {TYPES'02},
+  PUBLISHER = SV,
+  SERIES    = LNCS,
+  VOLUME    = {2646},
+  YEAR      = {2003}
+}
+
+@TECHREPORT{CoC89,
+        AUTHOR             = {Projet Formel},
+        INSTITUTION        = {INRIA},
+        NUMBER             = {110},
+        TITLE              = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}},
+        YEAR               = {1989}
+}
+
+@INPROCEEDINGS{CoHu85a,
+        AUTHOR             = {Th. Coquand and G. Huet},
+        ADDRESS            = {Linz},
+        BOOKTITLE          = {EUROCAL'85},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}},
+        VOLUME             = {203},
+        YEAR               = {1985}
+}
+
+@INPROCEEDINGS{CoHu85b,
+        AUTHOR             = {Th. Coquand and G. Huet},
+        BOOKTITLE          = {Logic Colloquium'85},
+        EDITOR             = {The Paris Logic Group},
+        PUBLISHER          = {North-Holland},
+        TITLE              = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}},
+        YEAR               = {1987}
+}
+
+@ARTICLE{CoHu86,
+        AUTHOR             = {Th. Coquand and G. Huet},
+        JOURNAL            = {Information and Computation},
+        NUMBER             = {2/3},
+        TITLE              = {The {Calculus of Constructions}},
+        VOLUME             = {76},
+        YEAR               = {1988}
+}
+
+@INPROCEEDINGS{CoPa89,
+        AUTHOR             = {Th. Coquand and C. Paulin-Mohring},
+        BOOKTITLE          = {Proceedings of Colog'88},
+        EDITOR             = {P. Martin-L\"of and G. Mints},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {Inductively defined types},
+        VOLUME             = {417},
+        YEAR               = {1990}
+}
+
+@BOOK{Con86,
+        AUTHOR             = {R.L. {Constable et al.}},
+        PUBLISHER          = {Prentice-Hall},
+        TITLE              = {{Implementing Mathematics with the Nuprl Proof Development System}},
+        YEAR               = {1986}
+}
+
+@PHDTHESIS{Coq85,
+        AUTHOR             = {Th. Coquand},
+        MONTH              = jan,
+        SCHOOL             = {Universit\'e Paris~7},
+        TITLE              = {Une Th\'eorie des Constructions},
+        YEAR               = {1985}
+}
+
+@INPROCEEDINGS{Coq86,
+        AUTHOR             = {Th. Coquand},
+        ADDRESS            = {Cambridge, MA},
+        BOOKTITLE          = {Symposium on Logic in Computer Science},
+        PUBLISHER          = {IEEE Computer Society Press},
+        TITLE              = {{An Analysis of Girard's Paradox}},
+        YEAR               = {1986}
+}
+
+@INPROCEEDINGS{Coq90,
+        AUTHOR             = {Th. Coquand},
+        BOOKTITLE          = {Logic and Computer Science},
+        EDITOR             = {P. Oddifredi},
+        NOTE               = {INRIA Research Report 1088, also in~\cite{CoC89}},
+        PUBLISHER          = {Academic Press},
+        TITLE              = {{Metamathematical Investigations of a Calculus of Constructions}},
+        YEAR               = {1990}
+}
+
+@INPROCEEDINGS{Coq91,
+        AUTHOR             = {Th. Coquand},
+        BOOKTITLE          = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science},
+        TITLE              = {{A New Paradox in Type Theory}},
+        MONTH              = {August},
+        YEAR               = {1991}
+}
+
+@INPROCEEDINGS{Coq92,
+        AUTHOR             = {Th. Coquand},
+        TITLE              = {{Pattern Matching with Dependent Types}},
+        YEAR               = {1992},
+        crossref = {Bastad92}
+}
+
+@INPROCEEDINGS{Coquand93,
+        AUTHOR             = {Th. Coquand},
+        TITLE              = {{Infinite Objects in Type Theory}},
+        YEAR               = {1993},
+        crossref = {Nijmegen93}
+}
+
+@MASTERSTHESIS{Cou94a,
+        AUTHOR             = {J. Courant},
+        MONTH              = sep,
+        SCHOOL             = {DEA d'Informatique, ENS Lyon},
+        TITLE              = {Explicitation de preuves par r\'ecurrence implicite},
+        YEAR               = {1994}
+}
+
+@INPROCEEDINGS{Del99,
+  author    = "Delahaye, D.",
+  title     = "Information Retrieval in a Coq Proof Library using
+               Type Isomorphisms",
+  booktitle = {Proceedings of TYPES'99, L\"okeberg},
+  publisher = SV,
+  series = lncs,
+  year      = "1999",
+  url      =
+    "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
+    "{\sf TYPES99-SIsos.ps.gz}"
+}
+
+@INPROCEEDINGS{Del00,
+  author    = "Delahaye, D.",
+  title     = "A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}",
+  booktitle = "Proceedings of Logic for Programming and Automated Reasoning
+               (LPAR), Reunion Island",
+  publisher = SV,
+  series =  LNCS,
+  volume    = "1955",
+  pages     = "85--95",
+  month     = "November",
+  year      = "2000",
+  url      =
+    "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
+    "{\sf LPAR2000-ltac.ps.gz}"
+}
+
+@INPROCEEDINGS{DelMay01,
+  author    = "Delahaye, D. and Mayero, M.",
+  title     = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels
+               en {\Coq}},
+  booktitle = "Journ\'ees Francophones des Langages Applicatifs, Pontarlier",
+  publisher = "INRIA",
+  month     = "Janvier",
+  year      = "2001",
+  url      =
+    "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
+    "{\sf JFLA2000-Field.ps.gz}"
+}
+
+@TECHREPORT{Dow90,
+        AUTHOR             = {G. Dowek},
+        INSTITUTION        = {INRIA},
+        NUMBER             = {1283},
+        TITLE              = {Naming and Scoping in a Mathematical Vernacular},
+        TYPE               = {Research Report},
+        YEAR               = {1990}
+}
+
+@ARTICLE{Dow91a,
+        AUTHOR             = {G. Dowek},
+        JOURNAL            = {Compte-Rendus de l'Acad\'emie des Sciences},
+        NOTE               = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors},
+        NUMBER             = {12},
+        PAGES              = {951--956},
+        TITLE              = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, 
+        VOLUME             = {I, 312},
+        YEAR               = {1991}
+}		  
+
+@INPROCEEDINGS{Dow91b,
+        AUTHOR             = {G. Dowek},
+        BOOKTITLE          = {Proceedings of Mathematical Foundation of Computer Science},
+        NOTE               = {Also INRIA Research Report},
+        PAGES              = {151--160},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi},
+        VOLUME             = {520},
+        YEAR               = {1991}
+}
+                  
+@PHDTHESIS{Dow91c,
+        AUTHOR             = {G. Dowek},
+        MONTH              = dec,
+        SCHOOL             = {Universit\'e Paris 7},
+        TITLE              = {D\'emonstration automatique dans le Calcul des Constructions},
+        YEAR               = {1991}
+}
+
+@article{Dow92a,
+        AUTHOR             = {G. Dowek},
+        TITLE              = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable},
+        YEAR               = 1993,
+        journal = tcs,
+        volume = 107,
+        number = 2,
+        pages = {349-356}
+}
+
+
+@ARTICLE{Dow94a,
+        AUTHOR             = {G. Dowek},
+        JOURNAL            = {Annals of Pure and Applied Logic},
+        VOLUME             = {69},
+        PAGES              = {135--155},
+        TITLE              = {Third order matching is decidable},
+        YEAR               = {1994}
+}
+
+@INPROCEEDINGS{Dow94b,
+        AUTHOR             = {G. Dowek},
+        BOOKTITLE          = {Proceedings of the second international conference on typed lambda calculus and applications},
+        TITLE              = {Lambda-calculus, Combinators and the Comprehension Schema},
+        YEAR               = {1995}
+}
+
+@INPROCEEDINGS{Dyb91,
+        AUTHOR             = {P. Dybjer},
+        BOOKTITLE          = {Logical Frameworks},
+        EDITOR             = {G. Huet and G. Plotkin},
+        PAGES              = {59--79},
+        PUBLISHER          = {Cambridge University Press},
+        TITLE              = {Inductive sets and families in {Martin-L{\"o}f's}
+ Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, 
+        VOLUME             = {14},
+        YEAR               = {1991}
+}
+
+@ARTICLE{Dyc92,
+        AUTHOR             = {Roy Dyckhoff},
+        JOURNAL            = {The Journal of Symbolic Logic},
+        MONTH              = sep,
+        NUMBER             = {3},
+        TITLE              = {Contraction-free sequent calculi for intuitionistic logic},
+        VOLUME             = {57},
+        YEAR               = {1992}
+}
+
+@MASTERSTHESIS{Fil94,
+        AUTHOR             = {J.-C. Filli\^atre},
+        MONTH              = sep,
+        SCHOOL             = {DEA d'Informatique, ENS Lyon},
+        TITLE              = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. {\'E}tude et impl\'ementation dans le syst\`eme {\Coq}},
+        YEAR               = {1994}
+}
+
+@TECHREPORT{Filliatre95,
+        AUTHOR             = {J.-C. Filli\^atre},
+        INSTITUTION        = {LIP-ENS-Lyon},
+        TITLE              = {A decision procedure for Direct Predicate Calculus},
+        TYPE               = {Research report},
+        NUMBER             = {96--25},
+        YEAR               = {1995}
+}
+
+@Article{Filliatre03jfp,
+  author = 	 {J.-C. Filli{\^a}tre},
+  title = 	 {Verification of Non-Functional Programs 
+                   using Interpretations in Type Theory},
+  journal =      jfp,
+  volume =       13,
+  number =       4,
+  pages =        {709--745},
+  month =	 jul,
+  year =	 2003,
+  note = 	 {[English translation of \cite{Filliatre99}]},
+  url =          {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz},
+  topics =       "team, lri",
+  type_publi =   "irevcomlec"
+}
+
+
+@PhdThesis{Filliatre99,
+  author = 	 {J.-C. Filli\^atre},
+  title = 	 {Preuve de programmes imp\'eratifs en th\'eorie des types},
+  type =         {Th{\`e}se de Doctorat},
+  school = 	 {Universit\'e Paris-Sud},
+  year = 	 1999,
+  month =	 {July},
+  url =         {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}}
+}
+
+@Unpublished{Filliatre99c,
+  author = 	 {J.-C. Filli\^atre},
+  title = 	 {{Formal Proof of a Program: Find}},
+  month =        {January},
+  year =         2000,
+  note = 	 {Submitted to \emph{Science of Computer Programming}},
+  url =         {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}}
+}
+
+@InProceedings{FilliatreMagaud99,
+  author = 	 {J.-C. Filli\^atre and N. Magaud},
+  title = 	 {Certification of sorting algorithms in the system {\Coq}},
+  booktitle =    {Theorem Proving in Higher Order Logics: 
+                  Emerging Trends},
+  year =	 1999,
+  url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}}
+}
+
+@UNPUBLISHED{Fle90,
+        AUTHOR             = {E. Fleury},
+        MONTH              = jul,
+        NOTE               = {Rapport de Stage},
+        TITLE              = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}},
+        YEAR               = {1990}
+}
+
+@BOOK{Fourier,
+        AUTHOR             = {Jean-Baptiste-Joseph Fourier},
+        PUBLISHER          = {Gauthier-Villars},
+        TITLE              = {Fourier's method to solve linear 
+                              inequations/equations systems.},
+        YEAR               = {1890}
+}
+
+@INPROCEEDINGS{Gim94,
+        AUTHOR             = {E. Gim\'enez},
+        BOOKTITLE          = {Types'94 : Types for Proofs and Programs},
+        NOTE               = {Extended version in LIP research report 95-07, ENS Lyon},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {Codifying guarded definitions with recursive schemes},
+        VOLUME             = {996},
+        YEAR               = {1994}
+}
+
+@TechReport{Gim98,
+  author = 	 {E. Gim\'enez},
+  title = 	 {A Tutorial on Recursive Types in Coq},
+  institution =  {INRIA},
+  year = 	 1998,
+  month =	 mar
+}
+
+@INPROCEEDINGS{Gimenez95b,
+        AUTHOR             = {E. Gim\'enez},
+        BOOKTITLE          = {Workshop on Types for Proofs and Programs},
+        SERIES             = LNCS,
+        NUMBER             = {1158},
+        PAGES              = {135-152},
+        TITLE              = {An application of co-Inductive types in Coq: 
+		               verification of the Alternating Bit Protocol},
+        EDITORS            = {S. Berardi and M. Coppo},
+        PUBLISHER          = SV,
+        YEAR               = {1995}
+}
+
+@INPROCEEDINGS{Gir70,
+        AUTHOR             = {J.-Y. Girard},
+        BOOKTITLE          = {Proceedings of the 2nd Scandinavian Logic Symposium},
+        PUBLISHER          = {North-Holland},
+        TITLE              = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types},
+        YEAR               = {1970}
+}
+
+@PHDTHESIS{Gir72,
+        AUTHOR             = {J.-Y. Girard},
+        SCHOOL             = {Universit\'e Paris~7},
+        TITLE              = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur},
+        YEAR               = {1972}
+}
+
+
+
+@BOOK{Gir89,
+        AUTHOR             = {J.-Y. Girard and Y. Lafont and P. Taylor},
+        PUBLISHER          = {Cambridge University Press},
+        SERIES             = {Cambridge Tracts in Theoretical Computer Science 7},
+        TITLE              = {Proofs and Types},
+        YEAR               = {1989}
+}
+
+@TechReport{Har95,
+  author = 	 {John Harrison},
+  title = 	 {Metatheory and Reflection in Theorem Proving: A Survey and Critique},
+  institution =  {SRI International Cambridge Computer Science Research Centre,},
+  year = 	 1995,
+  type =	 {Technical Report},
+  number =	 {CRC-053},
+  abstract =	 {http://www.cl.cam.ac.uk/users/jrh/papers.html}
+}
+
+@MASTERSTHESIS{Hir94,
+        AUTHOR             = {D. Hirschkoff},
+        MONTH              = sep,
+        SCHOOL             = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
+        TITLE              = {{\'E}criture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
+        YEAR               = {1994}
+}
+
+@INPROCEEDINGS{HofStr98,
+        AUTHOR        = {Martin Hofmann and Thomas Streicher},
+        TITLE         = {The groupoid interpretation of type theory},
+        BOOKTITLE     = {Proceedings of the meeting Twenty-five years of constructive type theory},
+        PUBLISHER     = {Oxford University Press},
+        YEAR          = {1998}
+} 
+
+@INCOLLECTION{How80,
+        AUTHOR             = {W.A. Howard},
+        BOOKTITLE          = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
+        EDITOR             = {J.P. Seldin and J.R. Hindley},
+        NOTE               = {Unpublished 1969 Manuscript},
+        PUBLISHER          = {Academic Press},
+        TITLE              = {The Formulae-as-Types Notion of Constructions},
+        YEAR               = {1980}
+}
+
+
+
+@InProceedings{Hue87tapsoft,
+  author = 	 {G. Huet},
+  title = 	 {Programming of Future Generation Computers},
+  booktitle = 	 {Proceedings of TAPSOFT87},
+       series = LNCS,
+        volume = 249,
+  pages =	 {276--286},
+  year =	 1987,
+  publisher =	 SV
+}
+
+@INPROCEEDINGS{Hue87,
+        AUTHOR             = {G. Huet},
+        BOOKTITLE          = {Programming of Future Generation Computers},
+        EDITOR             = {K. Fuchi and M. Nivat},
+        NOTE               = {Also in \cite{Hue87tapsoft}},
+        PUBLISHER          = {Elsevier Science},
+        TITLE              = {Induction Principles Formalized in the {Calculus of Constructions}},
+        YEAR               = {1988}
+}
+
+
+
+@INPROCEEDINGS{Hue88,
+        AUTHOR             = {G. Huet},
+        BOOKTITLE          = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
+        EDITOR             = {R. Narasimhan},
+        NOTE               = {Also in~\cite{CoC89}},
+        PUBLISHER          = {World Scientific Publishing},
+        TITLE              = {{The Constructive Engine}},
+        YEAR               = {1989}
+}
+
+@BOOK{Hue89,
+        EDITOR             = {G. Huet},
+        PUBLISHER          = {Addison-Wesley},
+        SERIES             = {The UT Year of Programming Series},
+        TITLE              = {Logical Foundations of Functional Programming},
+        YEAR               = {1989}
+}
+
+@INPROCEEDINGS{Hue92,
+        AUTHOR             = {G. Huet},
+        BOOKTITLE          = {Proceedings of 12th FST/TCS Conference, New Delhi},
+        PAGES              = {229--240},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {The Gallina Specification Language : A case study},
+        VOLUME             = {652},
+        YEAR               = {1992}
+}
+
+@ARTICLE{Hue94,
+        AUTHOR             = {G. Huet},
+        JOURNAL            = {J. Functional Programming},
+        PAGES              = {371--394},
+        PUBLISHER          = {Cambridge University Press},
+        TITLE              = {Residual theory in $\lambda$-calculus: a formal development},
+        VOLUME             = {4,3},
+        YEAR               = {1994}
+}
+
+@INCOLLECTION{HuetLevy79,
+        AUTHOR             = {G. Huet and J.-J. L\'{e}vy},
+        TITLE              = {Call by Need Computations in Non-Ambigous
+Linear Term Rewriting Systems},
+        NOTE               = {Also research report 359, INRIA, 1979},
+        BOOKTITLE          = {Computational Logic, Essays in Honor of
+Alan Robinson},
+        EDITOR             = {J.-L. Lassez and G. Plotkin},
+        PUBLISHER          = {The MIT press},
+        YEAR               = {1991}
+}
+
+@ARTICLE{KeWe84,
+        AUTHOR             = {J. Ketonen and R. Weyhrauch},
+        JOURNAL            = {Theoretical Computer Science},
+        PAGES              = {297--307},
+        TITLE              = {A decidable fragment of {P}redicate {C}alculus},
+        VOLUME             = {32},
+        YEAR               = {1984}
+}
+
+@BOOK{Kle52,
+        AUTHOR             = {S.C. Kleene},
+        PUBLISHER          = {North-Holland},
+        SERIES             = {Bibliotheca Mathematica},
+        TITLE              = {Introduction to Metamathematics},
+        YEAR               = {1952}
+}
+
+@BOOK{Kri90,
+        AUTHOR             = {J.-L. Krivine},
+        PUBLISHER          = {Masson},
+        SERIES             = {Etudes et recherche en informatique},
+        TITLE              = {Lambda-calcul {types et mod\`eles}},
+        YEAR               = {1990}
+}
+
+@BOOK{LE92,
+        EDITOR             = {G. Huet and G. Plotkin},
+        PUBLISHER          = {Cambridge University Press},
+        TITLE              = {Logical Environments},
+        YEAR               = {1992}
+}
+
+@BOOK{LF91,
+        EDITOR             = {G. Huet and G. Plotkin},
+        PUBLISHER          = {Cambridge University Press},
+        TITLE              = {Logical Frameworks},
+        YEAR               = {1991}
+}
+
+@ARTICLE{Laville91,
+        AUTHOR             = {A. Laville},
+        TITLE              = {Comparison of Priority Rules in Pattern
+Matching and Term Rewriting},
+        JOURNAL            = {Journal of Symbolic Computation},
+        VOLUME             = {11},
+        PAGES              = {321--347},
+        YEAR               = {1991}
+}
+
+@INPROCEEDINGS{LePa94,
+        AUTHOR             = {F. Leclerc and C. Paulin-Mohring},
+        BOOKTITLE          = {{Types for Proofs and Programs, Types' 93}},
+        EDITOR             = {H. Barendregt and T. Nipkow},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        TITLE              = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}},
+        VOLUME             = {806},
+        YEAR               = {1994}
+}
+
+@TECHREPORT{Leroy90,
+        AUTHOR             = {X. Leroy},
+        TITLE              = {The {ZINC} experiment: an economical implementation
+of the {ML} language},
+        INSTITUTION        = {INRIA},
+        NUMBER             = {117},
+        YEAR               = {1990}
+}
+
+@INPROCEEDINGS{Let02,
+        author          = {P. Letouzey},
+        title           = {A New Extraction for Coq},
+        booktitle       = {Proceedings of the TYPES'2002 workshop},
+        year            = 2002,
+        note            = {to appear},
+        url            = {draft at \url{http://www.lri.fr/~letouzey/download/extraction2002.ps.gz}}
+}
+
+@BOOK{MaL84,
+        AUTHOR             = {{P. Martin-L\"of}},
+        PUBLISHER          = {Bibliopolis},
+        SERIES             = {Studies in Proof Theory},
+        TITLE              = {Intuitionistic Type Theory},
+        YEAR               = {1984}
+}
+
+@ARTICLE{MaSi94,
+        AUTHOR             = {P. Manoury and M. Simonot},
+        JOURNAL            = {TCS},
+        TITLE              = {Automatizing termination proof of recursively defined function},
+        YEAR               = {To appear}
+}
+
+@INPROCEEDINGS{Moh89a,
+        AUTHOR             = {C. Paulin-Mohring},
+        ADDRESS            = {Austin},
+        BOOKTITLE          = {Sixteenth Annual ACM Symposium on Principles of Programming Languages},
+        MONTH              = jan,
+        PUBLISHER          = {ACM},
+        TITLE              = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}},
+        YEAR               = {1989}
+}
+
+@PHDTHESIS{Moh89b,
+        AUTHOR             = {C. Paulin-Mohring},
+        MONTH              = jan,
+        SCHOOL             = {{Universit\'e Paris 7}},
+        TITLE              = {Extraction de programmes dans le {Calcul des Constructions}},
+        YEAR               = {1989}
+}
+
+@INPROCEEDINGS{Moh93,
+        AUTHOR             = {C. Paulin-Mohring},
+        BOOKTITLE          = {Proceedings of the conference Typed Lambda Calculi and Applications},
+        EDITOR             = {M. Bezem and J.-F. Groote},
+        NOTE               = {Also LIP research report 92-49, ENS Lyon},
+        NUMBER             = {664},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        TITLE              = {{Inductive Definitions in the System Coq - Rules and Properties}},
+        YEAR               = {1993}
+}
+
+@BOOK{Moh97,
+        AUTHOR             = {C. Paulin-Mohring},
+        MONTH              = jan,
+        PUBLISHER          = {{ENS Lyon}},
+        TITLE              = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}},
+        YEAR               = {1997}
+}
+
+@MASTERSTHESIS{Mun94,
+        AUTHOR             = {C. Mu{\~n}oz},
+        MONTH              = sep,
+        SCHOOL             = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
+        TITLE              = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
+        YEAR               = {1994}
+}
+
+@PHDTHESIS{Mun97d,
+        AUTHOR = "C. Mu{\~{n}}oz",
+        TITLE = "Un calcul de substitutions pour la repr\'esentation
+                  de preuves partielles en th\'eorie de types",
+        SCHOOL = {Universit\'e Paris 7},
+        YEAR = "1997",
+        Note = {Version en anglais disponible comme rapport de 
+                recherche INRIA RR-3309},        
+        Type = {Th\`ese de Doctorat}
+}
+
+@BOOK{NoPS90,
+        AUTHOR             = {B. {Nordstr\"om} and K. Peterson and J. Smith},
+        BOOKTITLE          = {Information Processing 83},
+        PUBLISHER          = {Oxford Science Publications},
+        SERIES             = {International Series of Monographs on Computer Science},
+        TITLE              = {Programming in {Martin-L\"of's} Type Theory},
+        YEAR               = {1990}
+}
+
+@ARTICLE{Nor88,
+        AUTHOR             = {B. {Nordstr\"om}},
+        JOURNAL            = {BIT},
+        TITLE              = {Terminating General Recursion},
+        VOLUME             = {28},
+        YEAR               = {1988}
+}
+
+@BOOK{Odi90,
+        EDITOR             = {P. Odifreddi},
+        PUBLISHER          = {Academic Press},
+        TITLE              = {Logic and Computer Science},
+        YEAR               = {1990}
+}
+
+@INPROCEEDINGS{PaMS92,
+        AUTHOR             = {M. Parigot and P. Manoury and M. Simonot},
+        ADDRESS            = {St. Petersburg, Russia},
+        BOOKTITLE          = {Logic Programming and automated reasoning},
+        EDITOR             = {A. Voronkov},
+        MONTH              = jul,
+        NUMBER             = {624},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        TITLE              = {{ProPre : A Programming language with proofs}},
+        YEAR               = {1992}
+}
+
+@ARTICLE{PaWe92,
+        AUTHOR             = {C. Paulin-Mohring and B. Werner},
+        JOURNAL            = {Journal of Symbolic Computation},
+        PAGES              = {607--640},
+        TITLE              = {{Synthesis of ML programs in the system Coq}},
+        VOLUME             = {15},
+        YEAR               = {1993}
+}
+
+@ARTICLE{Par92,
+        AUTHOR             = {M. Parigot},
+        JOURNAL            = {Theoretical Computer Science},
+        NUMBER             = {2},
+        PAGES              = {335--356},
+        TITLE              = {{Recursive Programming with Proofs}},
+        VOLUME             = {94},
+        YEAR               = {1992}
+}
+
+@INPROCEEDINGS{Parent95b,
+        AUTHOR             = {C. Parent},
+        BOOKTITLE          = {{Mathematics of Program Construction'95}},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        TITLE              = {{Synthesizing proofs from programs in
+the Calculus of Inductive Constructions}},
+        VOLUME             = {947},
+        YEAR               = {1995}
+}
+
+@INPROCEEDINGS{Prasad93,
+        AUTHOR             = {K.V. Prasad},
+        BOOKTITLE          = {{Proceedings of CONCUR'93}},
+        PUBLISHER          = SV,
+        SERIES             = {LNCS},
+        TITLE              = {{Programming with broadcasts}},
+        VOLUME             = {715},
+        YEAR               = {1993}
+}
+
+@BOOK{RC95,
+  author = "di~Cosmo, R.",
+  title  = "Isomorphisms of Types: from $\lambda$-calculus to information
+            retrieval and language design",
+  series = "Progress in Theoretical Computer Science",
+  publisher = "Birkhauser",
+  year = "1995",
+  note = "ISBN-0-8176-3763-X"
+}
+
+@TECHREPORT{Rou92,
+        AUTHOR             = {J. Rouyer},
+        INSTITUTION        = {INRIA},
+        MONTH              = nov,
+        NUMBER             = {1795},
+        TITLE              = {{D{\'e}veloppement de l'Algorithme d'Unification dans le Calcul des Constructions}},
+        YEAR               = {1992}
+}
+
+@TECHREPORT{Saibi94,
+        AUTHOR             = {A. Sa\"{\i}bi},
+        INSTITUTION        = {INRIA},
+        MONTH              = dec,
+        NUMBER             = {2345},
+        TITLE              = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}},
+        YEAR               = {1994}
+}
+
+
+@MASTERSTHESIS{Ter92,
+        AUTHOR             = {D. Terrasse},
+        MONTH              = sep,
+        SCHOOL             = {IARFA},
+        TITLE              = {{Traduction de TYPOL en COQ. Application \`a Mini ML}},
+        YEAR               = {1992}
+}
+
+@TECHREPORT{ThBeKa92,
+        AUTHOR             = {L. Th\'ery and Y. Bertot and G. Kahn},
+        INSTITUTION        = {INRIA Sophia},
+        MONTH              = may,
+        NUMBER             = {1684},
+        TITLE              = {Real theorem provers deserve real user-interfaces},
+        TYPE               = {Research Report},
+        YEAR               = {1992}
+}
+
+@BOOK{TrDa89,
+        AUTHOR             = {A.S. Troelstra and D. van Dalen},
+        PUBLISHER          = {North-Holland},
+        SERIES             = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123},
+        TITLE              = {Constructivism in Mathematics, an introduction},
+        YEAR               = {1988}
+}
+
+@PHDTHESIS{Wer94,
+        AUTHOR             = {B. Werner},
+        SCHOOL             = {Universit\'e Paris 7},
+        TITLE              = {Une th\'eorie des constructions inductives},
+        TYPE               = {Th\`ese de Doctorat},
+        YEAR               = {1994}
+}
+
+@PHDTHESIS{Bar99,
+        AUTHOR             = {B. Barras},
+        SCHOOL             = {Universit\'e Paris 7},
+        TITLE              = {Auto-validation d'un système de preuves avec familles inductives},
+        TYPE               = {Th\`ese de Doctorat},
+        YEAR               = {1999}
+}
+
+@UNPUBLISHED{ddr98,
+	AUTHOR	           = {D. de Rauglaudre},
+        TITLE              = {Camlp4 version 1.07.2},
+        YEAR               = {1998},
+        NOTE               = {In Camlp4 distribution}
+}
+
+@ARTICLE{dowek93,
+        AUTHOR             = {G. Dowek},
+        TITLE              = {{A Complete Proof Synthesis Method for the Cube of Type Systems}},
+        JOURNAL            = {Journal Logic Computation},
+        VOLUME             = {3},
+        NUMBER             = {3},
+        PAGES              = {287--315},
+        MONTH              = {June},
+        YEAR               = {1993}
+}
+
+@INPROCEEDINGS{manoury94,
+        AUTHOR             = {P. Manoury},
+        TITLE              = {{A User's Friendly Syntax to Define
+Recursive Functions as Typed $\lambda-$Terms}},
+        BOOKTITLE          = {{Types for Proofs and Programs, TYPES'94}},
+        SERIES             = {LNCS},
+        VOLUME             = {996},
+        MONTH              = jun,
+        YEAR               = {1994}
+}
+
+@TECHREPORT{maranget94,
+        AUTHOR             = {L. Maranget},
+        INSTITUTION        = {INRIA},
+        NUMBER             = {2385},
+        TITLE              = {{Two Techniques for Compiling Lazy Pattern Matching}},
+        YEAR               = {1994}
+}
+
+@INPROCEEDINGS{puel-suarez90,
+        AUTHOR             = {L.Puel and A. Su\'arez},
+        BOOKTITLE          = {{Conference Lisp and Functional Programming}},
+        SERIES             = {ACM},
+        PUBLISHER          = SV,
+        TITLE              = {{Compiling Pattern Matching by Term
+Decomposition}},
+        YEAR               = {1990}
+}
+
+@MASTERSTHESIS{saidi94,
+        AUTHOR             = {H. Saidi},
+        MONTH              = sep,
+        SCHOOL             = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
+        TITLE              = {R\'esolution d'\'equations dans le syst\`eme T
+ de G\"odel},
+        YEAR               = {1994}
+}
+
+@misc{streicher93semantical,
+  author = "T. Streicher",
+  title = "Semantical Investigations into Intensional Type Theory",
+  note = "Habilitationsschrift, LMU Munchen.",
+  year = "1993" }
+
+
+
+@Misc{Pcoq,
+  author =	 {Lemme Team},
+  title =	 {Pcoq a graphical user-interface for {Coq}},
+  note =	 {\url{http://www-sop.inria.fr/lemme/pcoq/}}
+}
+
+
+@Misc{ProofGeneral,
+  author =	 {David Aspinall},
+  title =	 {Proof General},
+  note =	 {\url{http://proofgeneral.inf.ed.ac.uk/}}
+}
+
+
+
+@Book{CoqArt,
+  author =	 {Yves bertot and Pierre Castéran},
+  title = 	 {Coq'Art},
+  publisher = 	 {Springer-Verlag},
+  year = 	 2004,
+  note =	 {To appear}
+}
+
+@INCOLLECTION{wadler87,
+        AUTHOR             = {P. Wadler},
+        TITLE              = {Efficient  Compilation of Pattern Matching},
+        BOOKTITLE          = {The Implementation of Functional Programming
+Languages},
+        EDITOR             = {S.L. Peyton Jones},
+        PUBLISHER          = {Prentice-Hall},
+        YEAR               = {1987}
+}
+
+
+@COMMENT{cross-references, must be at end}
+
+@BOOK{Bastad92,
+        EDITOR             = {B. Nordstr\"om and K. Petersson and G. Plotkin},
+        PUBLISHER          = {Available by ftp at site ftp.inria.fr},
+        TITLE              = {Proceedings of the 1992 Workshop on Types for Proofs and Programs},
+        YEAR               = {1992}
+}
+
+@BOOK{Nijmegen93,
+        EDITOR             = {H. Barendregt and T. Nipkow},
+        PUBLISHER          = SV,
+        SERIES             = LNCS,
+        TITLE              = {Types for Proofs and Programs},
+        VOLUME             = {806},
+        YEAR               = {1994}
+}
+
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index b031694de8..b6aea67baa 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -7,8 +7,8 @@
 \usepackage{amssymb}
 \usepackage{url}
 \usepackage{multicol}
+\usepackage{hevea}
 \usepackage{fullpage}
-%\usepackage{hevea}
 %\usepackage[latin1]{inputenc}
 %\usepackage[english]{babel}
 
@@ -27,6 +27,11 @@
 \def\Ltac{\textsc{Ltac }}
 \def\CoqIde{\textsc{CoqIde }}
 
+\newcommand{\coqtt}[1]{{\tt #1}}
+\newcommand{\coqimp}{{\mbox{\tt ->}}}
+\newcommand{\coqequiv}{{\mbox{\tt <->}}}
+
+
 % macro pour les tactics
 \def\split{{\tt split }}
 \def\assumption{{\tt assumption }}
@@ -78,6 +83,26 @@
 \def\Defined{{\tt Defined }}
 \def\Qed{{\tt Qed }}
 \def\pattern{{\tt pattern }}
+\def\Type{{\tt Type }}
+\def\Prop{{\tt Prop }}
+\def\Set{{\tt Set }}
+
+
+\newcommand\vfile[2]{\ahref{#1}{\tt {#2}.v}}
+\urldef{\InitWf}{\url}
+  {http://coq.inria.fr/library/Coq.Init.Wf.html}
+\urldef{\LogicBerardi}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.Berardi.html}
+\urldef{\LogicClassical}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.Classical.html}
+\urldef{\LogicClassicalFacts}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html}
+\urldef{\LogicProofIrrelevance}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.ProofIrrelevance.html}
+\urldef{\LogicEqdep}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.Eqdep.html}
+\urldef{\LogicEqdepDec}{\url}
+  {http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html}
 
 
 
@@ -147,12 +172,31 @@ of this tacit convention. In French, ``coq'' means rooster, and it
 sounds like the initials of the Calculus of Constructions CoC on which
 it is based.
 
+\Question{Is \Coq a theorem prover?}
+
+\Coq comes with a few decision procedures (on propositional
+calculus, Presburger arithmetic, ring and field simplification,
+resolution, ...) but the main style for proving theorems is
+interactively by using LCF-style tactics.
+
+
 \Question{What are the other theorem provers ?} 
 Many other theorem provers are available for use nowadays. 
 Isabelle, HOL, HOL Light, Lego, Nuprl, PVS are examples of provers that are fairly similar
 to \Coq by the way they interact with the user. Other relatives of
 \Coq are ACL2, Alfa, Elf, Kiv, Mizar, NqThm, $\Omega$mega\ldots
 
+\Question{What's the status of proofs in \Coq}
+
+{\Coq} proofs are build with tactics allowing both forward 
+reasoning (stating
+
+cannot be accepted without a proof expressed in the Calculus of
+Inductive Constructions. The correctness of a proof relies on a
+relatively small proof-checker at the kernel of \Coq (8000 lines of ML
+code). Even \Coq decision procedures are producing proofs which are
+double-checked by the kernel.
+
 
 \Question{Where can I find information about the theory behind \Coq ?}
 \begin{description}
@@ -175,7 +219,6 @@ annotated programs written in other languages.
 
 Estimation is about 100 regular users.
 
-
 \Question{How old is \Coq ?}
 The first official release of \Coq (v. 4.10) was distributed in 1989.
 
@@ -195,6 +238,27 @@ The first official release of \Coq (v. 4.10) was distributed in 1989.
 \item[Foc] The Foc project aims at building an environment to develop certified computer algebra libraries. 
 \end{description}
 
+\Question{What are the high-level tactics of \Coq}
+
+\begin{itemize}
+\item Decision of quantifier-free Presburger's Arithmetic
+\item Simplification of expressions on rings and fields
+\item Decision of closed systems of equations
+\item Semi-decision of first-order logic
+\item Prolog-style proof search, possibly involving equalities
+\end{itemize}
+
+\Question{What are the main libraries of \Coq}
+
+\begin{itemize}
+\item Basic Peano's arithmetic
+\item Binary integer numbers
+\item Real analysis
+\item Libraries for lists, boolean, maps.
+\item Libraries for relations, sets
+\end{itemize}
+
+
 \Question{What are the academic applications for \Coq ?}
 
 Coq is used by mathematicians for formalizing large parts of mathematics, by teachers, and computer scientists to prove programs and APIs.
@@ -285,9 +349,250 @@ Windows. The sources can be easily adapted to all platforms supporting Objective
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\section{Logic}
+
+
+
+\Question{What is the logic of \Coq?}
+
+\Coq is based on an axiom-free type theory called
+the Calculus of Inductive Constructions (see Coquand \cite{CoHu86}
+and Coquand--Paulin-Mohring \cite{CoPa89}). It includes higher-order
+functions and predicates, inductive and co-inductive datatypes and
+predicates, and a stratified hierarchy of sets.
+
+\Question{Is \Coq's logic intuitionistic or classical?}
+
+\Coq theory is basically intuitionistic
+(i.e. excluded-middle $A\lor\neg A$ is not granted by default) with
+the possibility to reason classically on demand by requiring an
+optional module stating $A\lor\neg A$.
+
+
+\Question{Can I define non-terminating programs in \Coq?}
+
+No, all programs in \Coq are terminating. Especially, loops
+must come with an evidence of their termination.
+
+
+\Question{What is Streicher's axiom $K$}
+\label{Streicher}
+
+Streicher's axiom $K$ \cite{HofStr98} asserts dependent
+elimination of reflexive equality proofs.
+
+\begin{coq_example*}
+Axiom Streicher_K :
+  forall (A:Type) (x:A) (P: x=x -> Prop),
+    P (refl_equal x) -> forall p: x=x, P p.
+\end{coq_example*}
+
+In the general case, axiom $K$ is an independent statement of the
+Calculus of Inductive Constructions.  However, it is true on decidable
+domains (see file \vfile{\LogicEqdepDec}{Eqdep\_dec}). It is also
+trivially a consequence of proof-irrelevance (see
+\ref{proof-irrelevance}) hence of classical logic.
+
+Axiom $K$ is equivalent to {\em Uniqueness of Identity Proofs} \cite{HofStr98}
+which states that
+
+\begin{coq_example*}
+Axiom UIP : forall (A:Set) (x y:A) (p1 p2: x=y), p1 = p2.
+\end{coq_example*}
+
+Axiom $K$ is also equivalent to {\em Uniqueness of Reflexive Identity Proofs} \cite{HofStr98}
+
+\begin{coq_example*}
+Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = refl_equal x.
+\end{coq_example*}
+
+Axiom $K$ is also equivalent to 
+
+\begin{coq_example*}
+Axiom
+  eq_rec_eq :
+    forall (A:Set) (x:A) (P: A->Set) (p:P x) (h: x=x),
+      p = eq_rect x P p x h.
+\end{coq_example*}
+
+It is also equivalent to the injectivity of dependent equality (dependent equality is itself equivalent to equality of dependent pairs).
+
+\begin{coq_example*}
+Inductive eq_dep (U:Set) (P:U -> Set) (p:U) (x:P p) :
+forall q:U, P q -> Prop :=
+    eq_dep_intro : eq_dep U P p x p x.
+Axiom
+  eq_dep_eq :
+    forall (U:Set) (u:U) (P:U -> Set) (p1 p2:P u),
+      eq_dep U P u p1 u p2 -> p1 = p2.
+\end{coq_example*}
+
+\subsection{Impredicativity}
+
+\Question{Why Injection does not work on impredicative {\tt Set}?}
+
+ E.g. in this case (this occurs only in the {\tt Set}-impredicative
+ variant of \Coq:
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Inductive I : Type :=
+  intro : forall k:Set, k -> I.
+Lemma eq_jdef : 
+   forall x y:nat, intro _ x = intro _ y -> x = y.
+Proof.
+   intros x y H; injection H.
+\end{coq_example*}
+
+ Injectivity of constructors is restricted to predicative types. If
+injectivity on large inductive types were not restricted, we would be
+allowed to derive an inconsistency (e.g. following the lines of
+Burali-Forti paradox). The question remains open whether injectivity
+is consistent on some large inductive types not expressive enough to
+encode known paradoxes (such as type I above).
+
+
+\Question{What is a "large inductive definition"?}
+
+ An inductive definition in {\Prop} pr {\Set} is called large
+if its constructors embed sets or propositions. As an example, here is
+a large inductive type:
 
+\begin{coq_example*}
+Inductive sigST (P:Set -> Set) : Type :=
+  existST : forall X:Set, P X -> sigST P.
+\end{coq_example*}
 
+In the {\tt Set} impredicative variant of {\Coq}, large inductive
+definitions in {\tt Set} have restricted elimination schemes to
+prevent inconsistencies. Especially, projecting the set or the
+proposition content of a large inductive definition is forbidden. If
+it were allowed, it would be possible to encode e.g. Burali-Forti
+paradox \cite{Gir70,Coq85}.
 
+\Question{Why is dependent elimination in Prop not
+available by default?}
+
+ 
+This is just because most of the time it is not needed. To derive a
+dependent elimination principle in {\tt Prop}, use the command {\tt Scheme} and
+apply the elimination scheme using the \verb=using= option of
+\verb=elim=, \verb=destruct= or \verb=induction=.
+
+
+\Question{Can I identify two functions that have the same behaviour (extensionality)?}
+
+ Extensionality of functions is an axiom in, say set theory,
+but from a programming point of view, extensionality cannot be {\em a
+priori} accepted since it would identify, say programs as mergesort
+and quicksort.
+
+%\begin{coq_example*}
+%  Axiom extensionality : (A,B:Set)(f,g:(A->B))(x:A)(f x)=(g x)->f=g.
+%\end{coq_example*}
+
+Let {\tt A}, {\tt B} be types. To deal with extensionality on 
+\verb=A->B=, the recommended approach is to define his
+own extensional equality on \verb=A->B=.
+
+\begin{coq_eval}
+Variables A B : Set.
+\end{coq_eval}
+
+\begin{coq_example*}
+Definition ext_eq (f g: A->B) := forall x:A, f x = g x.
+\end{coq_example*}
+
+and to reason on \verb=A->B= as a setoid (see the Chapter on
+Setoids in the Reference Manual).
+
+\Question{Is {\Type} impredicative (that is, letting
+\coqtt{T:=(X:Type)X->X}, can I apply an expression \coqtt{t} of type \coqtt{T} to \coqtt{T} itself)?}
+
+ No, {\Type} is stratified. This is hidden for the
+user, but {\Coq} internally maintains a set of constraints ensuring
+stratification.
+
+  If {\Type} were impredicative then Girard's systems $U-$ and $U$
+could be encoded in {\Coq} and it is known from Girard, Coquand,
+Hurkens and Miquel that systems $U-$ and $U$ are inconsistent [Girard
+1972, Coquand 1991, Hurkens 1993, Miquel 2001]. This encoding can be
+found in file {\tt Logic/Hurkens.v} of {\Coq} standard library.
+
+  For instance, when the user see {\tt forall (X:Type), X->X : Type}, each
+occurrence of \Type is implicitly bound to a different level, say
+$\alpha$ and $\beta$ and the actual statement is {\tt
+forall X:Type($\alpha$), X->X : Type($\beta$)} with the constraint
+$\alpha<\beta$.
+
+  When a statement violates a constraint, the message {\tt Universe
+inconsistency} appears. Example: {\tt fun (x:Type) (y:forall X:Type, X \coqimp X) => z x x}.
+
+
+\Question{I have two proofs of the same proposition. Can I prove they are equal?}
+\label{proof-irrelevance}
+
+ In the base {\Coq} system, the answer is no. However, if
+classical logic is set, the answer is yes for propositions in {\Prop}.
+
+More precisely, the equality of all proofs of a given proposition is called
+{\em proof-irrelevance}. Proof-irrelevance (in {\Prop}) can be assumed
+  without leading to contradiction in {\Coq}.
+
+  That classical logic (what can be assumed in {\Coq} by requiring the file
+  \vfile{\LogicClassical}{Classical}) implies proof-irrelevance is shown in files
+  \vfile{\LogicProofIrrelevance}{ProofIrrelevance} and \vfile{\LogicBerardi}{Berardi}.
+
+  Alternatively, propositional extensionality (i.e.  \coqtt{(A
+  \coqequiv B) \coqimp A=B}, defined in \vfile{\LogicClassicalFacts}{ClassicalFacts}),
+  also implies proof-irrelevance.
+
+%  It is an ongoing work of research to natively include proof
+%  irrelevance in {\Coq}.
+
+\Question{Can I prove that the second components of equal dependent
+pairs are equal?}
+
+ The answer is the same as for proofs of equality
+statements. It is provable if equality on the domain of the first
+component is decidable (look at \verb=inj_right_pair= from file
+\vfile{\LogicEqdepDec}{Eqdep\_dec}), but not provable in the general
+case. However, it is consistent (with the Calculus of Constructions)
+to assume it is true. The file \vfile{\LogicEqdep}{Eqdep} actually
+provides an axiom (equivalent to Streicher's axiom $K$) which entails
+the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}).
+
+\Question{I have two proofs of an equality statement. Can I prove they are 
+equal?}
+
+ Yes, if equality is decidable on the domain considered (which
+is the case for {\tt nat}, {\tt bool}, etc): see {\Coq} file
+\verb=Eqdep_dec.v=). No otherwise, unless
+assuming Streicher's axiom $K$ (see \cite{HofStr98}) or a more general
+assumption such as proof-irrelevance (see \ref{proof-irrelevance}) or
+classical logic.
+
+
+All of these statements can be found in file \vfile{\LogicEqdep}{Eqdep}.
+
+\Question{How is equational reasoning working in {\Coq}?}
+
+ \Coq comes with an internal notion of computation called
+{\em conversion} (e.g. $(x+1)+y$ is internally equivalent to
+$(x+y)+1$; similarly applying argument $a$ to a function mapping $x$
+to some expression $t$ converts to the expression $t$ where $x$ is
+replaced by $a$). This notion of conversion (which is decidable
+because {\Coq} programs are terminating) covers a certain part of
+equational reasoning but is limited to sequential evaluation of
+expressions of (not necessarily closed) programs. Besides conversion,
+equations have to be treated by hand or using specialised tactics.
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Talkin' with the Rooster}
 
 
@@ -872,12 +1177,10 @@ You can organize your proofs using the section mechanism of \Coq. Have
 a look at the manual for further information.
 
 
-\section{Inductive types}
-
-
-\Question{How can I define a fixpoint when no argument is structurally smaller ?}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Inductive and Coinductive types}
 
-todo
+\subsection{General}
 
 \Question{How can I prove that two constructors are different ?}
 
@@ -890,6 +1193,241 @@ discriminate.
 Qed.
 \end{coq_example}
 
+\Question{How to eliminate impossible cases of an inductive definition}
+
+Use {\tt inversion}.
+
+
+\Question{How can I prove that 2 terms in an inductive set are equal? Or different?}
+
+ Cf "Decide Equality" and "Discriminate" in the \ahref{\refman}{Reference Manual}.
+
+\Question{Why is the proof of \coqtt{0+n=n} on natural numbers
+trivial but the proof of \coqtt{n+0=n} is not?}
+
+ Since \coqtt{+} (\coqtt{plus}) on natural numbers is defined by analysis on its first argument
+
+\begin{coq_example}
+Print plus.
+\end{coq_example}
+
+\noindent the expression \coqtt{0+n} evaluates to \coqtt{n}. As {\Coq} reasons
+modulo evaluation of expressions, \coqtt{0+n} and \coqtt{n} are
+considered equal and the theorem \coqtt{0+n=n} is an instance of the
+reflexivity of equality. On the other side, \coqtt{n+0} does not
+evaluate to \coqtt{n} and a proof by induction on \coqtt{n} is
+necessary to trigger the evaluation of \coqtt{+}.
+
+
+\subsection{Recursion}
+
+\Question{Why can't I define a non terminating program?}
+
+ Because otherwise the decidability of the type-checking
+algorithm (which involves evaluation of programs) is not ensured.  On
+another side, if non terminating proofs were allowed, we could get a
+proof of {\tt False}:
+
+\begin{coq_example*}
+(* This is fortunately not allowed! *)
+Fixpoint InfiniteProof (n:nat) : False := InfiniteProof n.
+Theorem Paradox : False.
+Proof (InfiniteProof O).
+\end{coq_example*}
+
+
+\Question{Why only structurally well-founded loops are allowed?}
+
+ The structural order on inductive types is a simple and
+powerful notion of termination. The consistency of the Calculus of
+Inductive Constructions relies on it and another consistency proof
+would have to be made for stronger termination arguments (such
+as the termination of the evaluation of CIC programs themselves!).
+
+In spite of this, all non-pathological termination orders can be mapped
+to a structural order. Tools to do this are provided in the file 
+\vfile{\InitWf}{Wf} of the standard library of {\Coq}.
+
+\Question{How to define loops based on non structurally smaller
+recursive calls?}
+
+ The procedure is as follows (we consider the definition of {\tt
+mergesort} as an example).
+
+\begin{itemize}
+
+\item Define the termination order, say {\tt R} on the type {\tt A} of
+the arguments of the loop.
+
+\begin{coq_eval}
+Open Scope R_scope.
+Require Import List.
+\end{coq_eval}
+
+\begin{coq_example*}
+Definition R (a b:list nat) := length a < length b.
+\end{coq_example*}
+
+\item Prove that this order is well-founded (in fact that all elements in {\tt A} are accessible along {\tt R}).
+
+\begin{coq_example*}
+Lemma Rwf : well_founded (A:=R).
+\end{coq_example*}
+
+\item Define the step function (which needs proofs that recursive
+calls are on smaller arguments).
+
+\begin{coq_example*}
+Definition split (l : list nat) 
+   : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}
+   := (* ... *) .
+Definition concat (l1 l2 : list nat) : list nat := (* ... *) .
+Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) :=
+  let (lH1,lH2) := (split l) in
+  let (l1,H1) := lH1 in
+  let (l2,H2) := lH2 in
+  concat (f l1 H1) (f l2 H2).
+\end{coq_example*}
+
+\item Define the recursive function by fixpoint on the step function.
+
+\begin{coq_example*}
+Definition merge := Fix Rwf (fun _ => list nat) merge_step.
+\end{coq_example*}
+
+\end{itemize}
+
+\Question{What is behind these accessibility and well-foundedness proofs?}
+
+ Well-foundedness of some relation {\tt R} on some type {\tt A}
+is defined as the accessibility of all elements of {\tt A} along {\tt R}.
+
+\begin{coq_example}
+Print well_founded.
+Print Acc.
+\end{coq_example}
+
+The structure of the accessibility predicate is a well-founded tree
+branching at each node {\tt x} in {\tt A} along all the nodes {\tt x'}
+less than {\tt x} along {\tt R}. Any sequence of elements of {\tt A}
+decreasing along the order {\tt R} are branches in the accessibility
+tree. Hence any decreasing along {\tt R} is mapped into a structural
+decreasing in the accessibility tree of {\tt R}. This is emphasised in
+the definition of {\tt fix} which recurs not on its argument {\tt x:A}
+but on the accessibility of this argument along {\tt R}.
+
+See file \vfile{\InitWf}{Wf}.
+
+\Question{How to perform double induction?}
+
+ In general a double induction is simply solved by an induction on the
+first hypothesis followed by an inversion over the second
+hypothesis. Here is an example
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example}
+Inductive even : nat -> Prop :=
+  | even_O : even 0
+  | even_S : forall n:nat, even n -> even (S (S n)).
+
+Inductive odd : nat -> Prop :=
+  | odd_SO : odd 1
+  | odd_S : forall n:nat, odd n -> odd (S (S n)).
+
+Goal forall n:nat, even n -> odd n -> False.
+induction 1.
+  inversion 1.
+  inversion 1. apply IHeven; trivial.
+Qed.
+\end{coq_example}
+
+In case the type of the second induction hypothesis is not
+dependent, {\tt inversion} can just be replaced by {\tt destruct}.
+
+
+
+\Question{How to define a function by double recursion?}
+
+ The same trick applies, you can even use the pattern-matching
+compilation algorithm to do the work for you. Here is an example:
+
+\begin{coq_example}
+Fixpoint minus (n m:nat) {struct n} : nat :=
+  match n, m with
+  | O, _ => 0
+  | S k, O => S k
+  | S k, S l => minus k l
+  end.
+Print  minus.
+\end{coq_example}
+
+In case of dependencies in the type of the induction objects
+$t_1$ and $t_2$, an extra argument stating $t_1=t_2$ must be given to
+the fixpoint definition
+
+\Question{How to perform nested induction?}
+
+ To reason by nested induction, just reason by induction on the
+successive components.
+
+\begin{coq_eval}
+Require Import Arith.
+\end{coq_eval}
+
+\begin{coq_example}
+Infix "<" := lt (at level 50, no associativity).
+Infix "<=" := le (at level 50, no associativity).
+Lemma le_or_lt : forall n n0:nat, n0 < n \/ n <= n0.
+induction n; destruct n0; auto with arith.
+destruct (IHn n0); auto with arith.
+\end{coq_example}
+
+
+\Question{How to define a function by nested recursion?}
+
+ The same trick applies. Here is the example of Ackermann
+function.
+
+\begin{coq_example}
+Fixpoint ack (n:nat) : nat -> nat :=
+  match n with
+  | O => S
+  | S n' =>
+     (fix ack' (m:nat) : nat :=
+        match m with
+        | O => ack n' 1
+        | S m' => ack n' (ack' m')
+        end)
+  end.
+\end{coq_example}
+
+
+\subsection{Coinductive types}
+
+\Question{I have a cofixpoint t:=F(t) and I want to prove t=F(t). What is
+the simplest way?}
+
+ Just case-expand F(t) then complete by a trivial case analysis.
+Here is what it gives on e.g. the type of streams on naturals
+
+\begin{coq_example}
+CoInductive Stream (A:Set) : Set :=
+  Cons : A -> Stream A -> Stream A.
+CoFixpoint nats (n:nat) : Stream nat := Cons n (nats (S n)).
+Lemma Stream_unfold : 
+   forall n:nat, nats n = Cons n (nats (S n)).
+Proof.
+  intro;
+  change (nats n = match nats n with
+                  | Cons x s => Cons x s
+                  end).
+  case (nats n); reflexivity.
+Qed.
+\end{coq_example}
+
 
 
 
@@ -1009,7 +1547,125 @@ You have some examples of tactics written in Ocaml in the ``contrib'' directory
 
 \Question{How can I define vectors or lists of size n ?}
 
+\Question{How to prove that 2 sets are differents?}
+
+ You need to find a property true on one set and false on the
+other one. As an example we show how to prove that {\tt bool} and {\tt
+nat} are discriminable. As discrimination property we take the
+property to have no more than 2 elements.
+
+\begin{coq_example*}
+Theorem nat_bool_discr : bool <> nat.
+Proof.
+  pose (discr :=
+    fun X:Set =>
+      ~ (forall a b:X, ~ (forall x:X, x <> a -> x <> b -> False))).
+  intro Heq; assert (H: discr bool).
+  intro H; apply (H true false); destruct x; auto.
+  rewrite Heq in H; apply H; clear H.
+  destruct a; destruct b as [|n]; intro H0; eauto.
+  destruct n; [ apply (H0 2); discriminate | eauto ].
+Qed.
+\end{coq_example*}
 
+\Question{How to exploit equalities on sets}
+
+ To extract information from an equality on sets, you need to
+find a predicate of sets satisfied by the elements of the sets. As an
+example, let's consider the following theorem.
+
+\begin{coq_example*}
+Theorem le_le :
+  forall m n:nat,
+    {x : nat | x <= m} = {x : nat | x <= n} -> m = n.
+\end{coq_example*}
+
+A typical property is to have cardinality $n$.
+
+
+\Question{I have a problem of dependent elimination on
+proofs, how to solve it?}
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Inductive Def1 : Set := c1 : Def1.
+Inductive DefProp : Def1 -> Set :=
+  c2 : forall d:Def1, DefProp d.
+Inductive Comb : Set :=
+  c3 : forall d:Def1, DefProp d -> Comb.
+Lemma eq_comb :
+  forall (d1 d1':Def1) (d2:DefProp d1) (d2':DefProp d1'),
+    d1 = d1' -> c3 d1 d2 = c3 d1' d2'.
+\end{coq_example*}
+
+ You need to derive the dependent elimination
+scheme for DefProp by hand using {\coqtt Scheme}.
+
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+\begin{coq_example*}
+Scheme DefProp_elim := Induction for DefProp Sort Prop.
+Lemma eq_comb :
+  forall d1 d1':Def1,
+    d1 = d1' ->
+    forall (d2:DefProp d1) (d2':DefProp d1'), c3 d1 d2 = c3 d1' d2'.
+intros.
+destruct H.
+destruct d2 using DefProp_elim.
+destruct d2' using DefProp_elim.
+reflexivity.
+Qed.
+\end{coq_example*}
+
+
+\Question{And what if I want to prove the following?}
+
+\begin{coq_example*}
+Inductive natProp : nat -> Prop :=
+  | p0 : natProp 0
+  | pS : forall n:nat, natProp n -> natProp (S n).
+Inductive package : Set :=
+  pack : forall n:nat, natProp n -> package.
+Lemma eq_pack :
+ forall n n':nat,
+   n = n' ->
+   forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'.
+\end{coq_example*}
+
+
+
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+\begin{coq_example*}
+Scheme natProp_elim := Induction for natProp Sort Prop.
+Definition pack_S : package -> package.
+destruct 1.
+apply (pack (S n)).
+apply pS; assumption.
+Defined.
+Lemma eq_pack :
+  forall n n':nat,
+    n = n' ->
+    forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'.
+intros n n' Heq np np'.
+generalize dependent n'.
+induction np using natProp_elim.
+induction np' using natProp_elim; intros; auto.
+ discriminate Heq.
+induction np' using natProp_elim; intros; auto.
+ discriminate Heq.
+change (pack_S (pack n np) = pack_S (pack n0 np')).
+apply (f_equal (A:=package)).
+apply IHnp.
+auto.
+Qed.
+\end{coq_example*}
 
 
 
@@ -1225,6 +1881,34 @@ stated some local lemma, this speeds up the typing process.
 
 You can help coq using the \pattern tactic.
 
+\Question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?}
+
+ This is because \texttt{\{x:A|P x\}} is a notation for
+\texttt{sig (fun x:A => P x)}. Since {\Coq} does not reason up to
+$\eta$-conversion, this is different from \texttt{sig P}.
+
+
+\Question{I copy-paste a term and {\Coq} says it is not convertible
+  to the original term. Sometimes it even says the copied term is not
+well-typed.}
+
+ This is probably due to invisible implicit information (implicit
+arguments, coercions and Cases annotations) in the printed term, which
+is not re-synthetised from the copied-pasted term in the same way as
+it is in the original term.
+
+  Consider for instance {\tt (@eq Type True True)}. This term is
+printed as {\tt True=True} and re-parsed as {\tt (@eq Prop True
+True)}. The two terms are not convertible (hence they fool tactics
+like {\tt pattern}).
+
+  There is currently no satisfactory answer to the problem.
+ 
+  Due to coercions, one may even face type-checking errors. In some
+rare cases, the criterion to hide coercions is a bit too loosy, which
+may result in a typing error message if the parser is not able to find
+again the missing coercion.
+
 
 
 \section{Conclusion and Farewell.}