community review, solved a couple of TODO

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

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index fd1ef3b6e43ce3759a26cf340da90645fbbc5c27..fdd419029244ea369dbc9f925ef5588507677995 100644 (file)
--- a/helm/papers/matita/matita.bib
+++ b/helm/papers/matita/matita.bib
@@ -1,8 +1,8 @@
+
 @book{paramodulation,
   author = "Robert Nieuwenhuis and Alberto Rubio",
   title = "Paramodulation-based thorem proving",
   booktitle = "Handbook of Automated Reasoning",
-  editor = "John Alan Robinson and Andrei Voronkov",
   pages = "471--443",
   publisher = "Elsevier and MIT Press",
   year = 2001,
@@ -51,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",
@@ -77,7 +77,7 @@
 }
 
 @inproceedings{proof-by-pointing,
-  author = "Yves Bertot and Gilles Kahn and Laurent Théry",
+  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",
@@ -302,7 +302,7 @@
   title           = "{Interactive Theorem Proving and Program Development}",
   publisher       = {Springer Verlag},
   series          = {Texts in Theoretical Computer Science},
-  year            = 2004
+  year            = 2004,
   NOTE            = {ISBN-3-540-20854-2}
     
 }
@@ -321,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,
@@ -438,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",
@@ -1229,7 +1229,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",
 }
 
@@ -1588,7 +1588,7 @@ elettroniche}",
 @inproceedings{barthe95implicit,
     author = "Gilles Barthe",
     title = "Implicit Coercions in Type Systems",
-    booktitle = "{TYPES}",
+    booktitle = "Types for Proofs and Programs: International Workshop, {TYPES 1995}",
     pages = "1-15",
     year = "1995",
     url = "citeseer.ist.psu.edu/barthe95implicit.html" }