/me reviewed up to section 2 (included)

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

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index 12b28d754d1f6ce16cac06afc061667e0d7b21a9..8aa1c4882a5aecce42eec255e484ab6d85b44031 100644 (file)
--- a/helm/papers/matita/matita.bib
+++ b/helm/papers/matita/matita.bib
@@ -463,8 +463,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 +952,7 @@
 @misc{debrujinfactor,
  title = "The ``de Bruijn factor''",
  howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
+ year = {2000},
  author = "Freek Wiedijk",
 }
 
@@ -970,8 +971,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 +992,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 +1066,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 +1077,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,
@@ -1121,7 +1123,8 @@ 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}",
+ howpublished = "\\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}",
+ year = {2005},
  key = "OMDoc"
 }
 
@@ -1562,3 +1565,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" }
+