aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-14 22:18:08 +0000
committerGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-14 22:18:08 +0000
commit2d9566b5cc2c8bedc544cd6add8f000c8cc5013c (patch)
treeea1cccd8317010b4a7d90347d096d97824ef3190
parentab2c8b843cd81c2dc5febb4d51b4a55f808f88d1 (diff)
Ajout these Bruno
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8394 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xdoc/biblio.bib20
1 files changed, 18 insertions, 2 deletions
diff --git a/doc/biblio.bib b/doc/biblio.bib
index 96cf10028..8f38d2b60 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -1,4 +1,3 @@
-
@string{jfp = "Journal of Functional Programming"}
@STRING{lncs="Lecture Notes in Computer Science"}
@STRING{lnai="Lecture Notes in Artificial Intelligence"}
@@ -990,6 +989,14 @@ Automated Reasoning},
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},
@@ -1061,13 +1068,22 @@ Decomposition}},
}
-
@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},