/me reviewed section 3, here I go ...

[helm.git] / helm / papers / matita / matita.bib

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index 5402461e4ed5a7dc13434b14bc211514a457093f..bd7b0baee43f855c0ac9788228e5a7880b922609 100644 (file)
--- a/helm/papers/matita/matita.bib
+++ b/helm/papers/matita/matita.bib
@@ -1,4 +1,14 @@
 
+@book{paramodulation,
+  author = "Robert Nieuwenhuis and Alberto Rubio",
+  title = "Paramodulation-based thorem proving",
+  booktitle = "Handbook of Automated Reasoning",
+  pages = "471--443",
+  publisher = "Elsevier and MIT Press",
+  year = 2001,
+  NOTE = {ISBN-0-262-18223-8}
+}
+
 @inproceedings{latexmathml,
  author = {Luca Padovani},
  title = {On the Roles of LATEX and MathML in Encoding and Processing Mathematical Expressions},
@@ -67,12 +77,12 @@
 }
 
 @inproceedings{proof-by-pointing,
-  author = "Yves Bertot",
+  author = "Yves Bertot and Gilles Kahn and Laurent Théry",
   title = "Proof by Pointing",
   booktitle = "Symposium on Theoretical Aspects Computer Software (STACS)",
   series = "Lecture Notes in Computer Science",
   volume = "789",
-  year = 1993
+  year = 1994
 }
 
 @inproceedings{thery-cyp,
@@ -287,6 +297,16 @@
   year            = 1989
 }
 
+@book{CoqArt,
+  author          = "Yves Bertot and Pierre Castéran",
+  title           = "{Interactive Theorem Proving and Program Development}",
+  publisher       = {Springer Verlag},
+  series          = {Texts in Theoretical Computer Science},
+  year            = 2004,
+  NOTE            = {ISBN-3-540-20854-2}
+    
+}
+
 @inproceedings{proofgeneral,
   author          = "David Aspinall",
   title           = "{P}roof {G}eneral: A Generic Tool for Proof Development",
@@ -992,7 +1012,6 @@
 @misc{lego,
  title = "The {L}ego proof-assistant",
  howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
- url = "\url{http://www.dcs.ed.ac.uk/home/lego/}",
  key = "Lego"
 }
 
@@ -1566,3 +1585,11 @@ elettroniche}",
        year="1997"
        }
 
+@inproceedings{barthe95implicit,
+    author = "Gilles Barthe",
+    title = "Implicit Coercions in Type Systems",
+    booktitle = "{TYPES}",
+    pages = "1-15",
+    year = "1995",
+    url = "citeseer.ist.psu.edu/barthe95implicit.html" }
+