]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/papers/matita/matita.bib
/me reviewed up to section 2 (included)
[helm.git] / helm / papers / matita / matita.bib
index 9e74514b7404520a30ae58ac3acb7ad7134738ec..8aa1c4882a5aecce42eec255e484ab6d85b44031 100644 (file)
            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"
 }
 
 @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"
 @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"
 }
 
  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,
@@ -1078,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,
@@ -1566,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" }
+