X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.bib;h=19d2df5dc1fd6563a8e7a4b6b342ffbbd358448a;hb=c1986639552e01334a05db4236627a6c1ffacf21;hp=12b28d754d1f6ce16cac06afc061667e0d7b21a9;hpb=112afe13b5aef27425d1a0bc9c71a70b491069bf;p=helm.git

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index 12b28d754..19d2df5dc 100644
--- 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},
@@ -41,7 +51,7 @@
 }
 
 @inproceedings{thery-authoring,
-  author = "Laurent Th\`ery",
+  author = "Laurent {Th\'ery}",
   title = "Formal Proof Authoring: an Experiment",
   booktitle = "User Interface Design for Theorem Provers",
   editor = "David Aspinall and Christoph L{\"u}th",
@@ -67,12 +77,12 @@
 }
 
 @inproceedings{proof-by-pointing,
-  author = "Yves Bertot",
+  author = "Yves Bertot and Gilles Kahn and Laurent Th\'ery",
   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",
@@ -301,7 +321,7 @@
 @inproceedings{Gim94,
   author          = "Eduardo Gim\'enez",
   title           = "{Codifying guarded definitions with recursive schemes}",
-  booktitle       = "Types'94: Types for Proofs and Programs",
+  booktitle       = "Types for Proofs and Programs: International Workshop, {TYPES '94}",
   series          = "LNCS",
   volume          = 996,
   year            = 1994,
@@ -418,7 +438,7 @@
   author = "Alexandre Miquel and Benjamin Werner",
   title = "The Not So Simple Proof-Irrelevant Model of {CC}",
   editor =    "Herman Geuvers and Freek Wiedijk",
-  booktitle = "Types for Proofs and Programs: International Workshop, TYPES 2002",
+  booktitle = "Types for Proofs and Programs: International Workshop, {TYPES 2002}",
   pages =     "240--258",
   volume =    "LNCS, 2646",
   publisher = "Springer-Verlag",
@@ -463,8 +483,8 @@
 	    and Enrico Tassi and Stefano Zacchiroli",
   title =        "A content based mathematical search engine: Whelp",
   booktitle =    "Post-proceedings of the Types 2004 International Conference",
-  volume =       "LNCS, (to appear)",
-  pages =        "xxx--xxx",
+  volume =       "LNCS, 3839",
+  pages =        "17--32",
   publisher =    "Springer-Verlag",
   year =         "2004"
 }
@@ -952,6 +972,7 @@
 @misc{debrujinfactor,
  title = "The ``de Bruijn factor''",
  howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
+ year = {2000},
  author = "Freek Wiedijk",
 }
 
@@ -970,8 +991,9 @@
 
 @misc{CoqManual,
  title = "The {C}oq Proof Assistant Reference Manual",
- author = "The Coq Development Team",
+ author = "{The Coq Development Team}",
  howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
+ year = {2005},
  key = "CoqManual"
 }
 
@@ -990,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"
 }
 
@@ -1065,8 +1086,9 @@
  title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
  editor="{Patrick Ion} and others",
  howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
+ year = {2003},
  url = "\url{http://www.w3.org/TR/MathML2}",
- key = "Mathematical"
+ key = "MathML"
 }
 
 @misc{xml,
@@ -1075,7 +1097,7 @@ editor="{Tim Bray} and others",
  howpublished = "W3C Recommendation 10 February 1998,
                  \url{http://www.w3.org/TR/REC-xml}",
  url = "\url{http://www.w3.org/TR/REC-xml}",
- key = "Extensible"
+ key = "XML"
 }
 
 @misc{dom,
@@ -1120,8 +1142,10 @@ editor="{Tim Bray} and others",
 }
 
 @misc{omdoc,
- title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
- howpublished = "\\\url{http://www.mathweb.org/omdoc/omdoc.ps}",
+ title = "{OMDoc}: An Open Markup Format for Mathematical Documents 
+(Draft, Version 1.2)",
+ howpublished = "\\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.2.pdf}",
+ year = {2005},
  key = "OMDoc"
 }
 
@@ -1206,7 +1230,7 @@ editor="{Tim Bray} and others",
 		 and Claudio {Sacerdoti Coen} and Irene Schena",
   title =        "{XML}, Stylesheets and the re-mathematization
 		 of Formal Content",
-  booktitle =    "EXTREME",
+  booktitle =    "Electronic Proceedings of {EXTREME Markup Languages} 2001",
   year = "2001",
 }
 
@@ -1562,3 +1586,11 @@ elettroniche}",
 	year="1997"
 	}
 
+@inproceedings{barthe95implicit,
+    author = "Gilles Barthe",
+    title = "Implicit Coercions in Type Systems",
+    booktitle = "Types for Proofs and Programs: International Workshop, {TYPES 1995}",
+    pages = "1-15",
+    year = "1995",
+    url = "citeseer.ist.psu.edu/barthe95implicit.html" }
+