From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 doc/refman/biblio.bib | 82 ++++++++++++++++++++++++++++++---------------------
 1 file changed, 48 insertions(+), 34 deletions(-)

(limited to 'doc/refman/biblio.bib')

diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index b9a3a2c5..d16c82c5 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -100,26 +100,25 @@ Computer Architecture},
         YEAR               = {1992}
 }
 
-@inproceedings{Bou97,
-   title = {Using reflection to build efficient and certified decision procedure
+@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}
+   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
+@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,
@@ -297,6 +296,15 @@ s},
         crossref = {Nijmegen93}
 }
 
+@PHDTHESIS{Cor97,
+        AUTHOR             = {C. Cornes},
+        MONTH              = nov,
+        SCHOOL             = {{Universit\'e Paris 7}},
+        TITLE              = {Conception d'un langage de haut niveau de représentation de preuves},
+        TYPE               = {Th\`ese de Doctorat},
+        YEAR               = {1997}
+}
+
 @MASTERSTHESIS{Cou94a,
         AUTHOR             = {J. Courant},
         MONTH              = sep,
@@ -525,14 +533,23 @@ s},
         YEAR               = {1994}
 }
 
-@TechReport{Gim98,
-  author = 	 {E. Gim\'enez},
-  title = 	 {A Tutorial on Recursive Types in Coq},
-  institution =  {INRIA},
-  year = 	 1998,
-  month =	 mar
+@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},
@@ -607,8 +624,6 @@ s},
         YEAR               = {1980}
 }
 
-
-
 @InProceedings{Hue87tapsoft,
   author = 	 {G. Huet},
   title = 	 {Programming of Future Generation Computers},
@@ -630,8 +645,6 @@ s},
         YEAR               = {1988}
 }
 
-
-
 @INPROCEEDINGS{Hue88,
         AUTHOR             = {G. Huet},
         BOOKTITLE          = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
@@ -1115,15 +1128,16 @@ Decomposition}},
   note =	 {\url{http://proofgeneral.inf.ed.ac.uk/}}
 }
 
+@Book{CoqArt,
+   title = "Interactive Theorem Proving and Program Development.
+    Coq'Art: The Calculus of Inductive Constructions",
+   author = "Yves Bertot and Pierre Castéran",
+   publisher = "Springer Verlag",
+   series = "Texts in Theoretical Computer Science. An EATCS series", 
+ year = 2004
+  }
 
 
-@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},
-- 
cgit v1.2.3