snapshot

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

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index f98e9c431b865614f22e1fb814f43de6a161fc15..d82d7d4d9e50928dba91a3aa2b4f97ff87928ea8 100644 (file)
--- a/helm/papers/matita/matita.bib
+++ b/helm/papers/matita/matita.bib
@@ -1,4 +1,15 @@
 
+@inproceedings{latexmathml,
+ author = {Luca Padovani},
+ title = {On the Roles of LATEX and MathML in Encoding and Processing Mathematical Expressions},
+ booktitle = {MKM '03: Proceedings of the Second International Conference on Mathematical Knowledge Management},
+ year = {2003},
+ isbn = {3-540-00568-4},
+ pages = {66--79},
+ publisher = {Springer-Verlag},
+ address = {London, UK},
+}
+
 @inproceedings{gmetadom,
   author = "Luca Padovani and Claudio Sacerdoti Coen and Stefano Zacchiroli",
   title = "A Generative Approach to the Implementation of Language Bindings for the Document Object Model",
@@ -538,7 +549,6 @@
   year =         "2003",
 }
 
-
 @article{asperti-categorical-understanding,
   author = "Andrea Asperti",
   title = "A categorical understanding of environment machines",
@@ -568,6 +578,15 @@
   year = "1999"
 }
 
+@TechReport{ctcoq2,
+  author =       "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
+  title =        "Real Theorem Provers Deserve Real User-Interfaces",
+  month =        may,
+  year =         "1992",
+  institution =  "INRIA",
+  number =       "{Inria Research Report 1684}"
+}
+
 @article{ctcoq3,
   author = "Yves Bertot and Laurent Th\'ery",
   title = "A Generic Approach to Building User Interfaces for Theorem Provers",
@@ -912,6 +931,15 @@
   year =         1998
 }
 
+@misc{content-centric,
+ author = "Andrea Asperti and Luca padovani and Claudio Sacerdoti Coen
+           and irene Schena",
+ title = "Content-centric Logical Envirnoments",
+ howpublished = "Short Presentation at the Fifteenth IEEE Symposium on Logic in Computer Science",
+ month = "June",
+ year = "2000",
+ key = "content centric"
+}
 
 @misc{mowgli-proposal,
  title = "The {MoWGLI Proposal}, {HTML} Version",
@@ -919,6 +947,12 @@
  key = "MoWGLI Proposal"
 }
 
+@misc{debrujinfactor,
+ title = "The ``de Bruijn factor''",
+ howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
+ author = "Freek Wiedijk",
+}
+
 @misc{mowgli-deliverables,
  title = "{MoWGLI} Project Deliverables",
  howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}",
@@ -932,6 +966,13 @@
  key = "ALF"
 }
 
+@misc{CoqManual,
+ title = "The {C}oq Proof Assistant Reference Manual",
+ author = "The Coq Development Team",
+ howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
+ key = "CoqManual"
+}
+
 @misc{Coq,
  title = "The {C}oq proof-assistant",
  howpublished = "\\\url{http://coq.inria.fr}",
@@ -970,6 +1011,17 @@
  key = "Isabelle"
 }
 
+@book{nuprl-book,
+  author =    "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and 
+               W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and 
+               T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
+               Scott F. Smith",
+  title =     "Implementing Mathematics with the {N}uprl Development System",
+  publisher = "Prentice-Hall",
+  year =      1986,
+  address =   "NJ"
+}
+
 @misc{nuprl,
  title = "The {NuPRL} proof-assistant",
  howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
@@ -1116,15 +1168,6 @@ editor="{Tim Bray} and others",
                   ({TPHOLS}'2000), Portland, Oregon, USA",
 }
 
-@TechReport{ctcoq2,
-  author =       "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
-  title =        "Real Theorem Provers Deserve Real User-Interfaces",
-  month =        may,
-  year =         "1992",
-  institution =  "INRIA",
-  number =       "{Inria Research Report 1684}"
-}
-
 @inproceedings{Ring,
   author =       "Samuel Boutin",
   title =        "Using Reflection to Build Efficient and Certified Decision