X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.bib;h=f2f024e718d66a979a6bd90e27acffdf6fddaa7a;hb=e67566145f090de0bfc28d4f1eea82a42c2e1ed1;hp=5b53ac0b9adbc95f16e08c610277006cce23b59d;hpb=af95120ce01907e21b53ebcf23e085590fa9eb04;p=helm.git

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index 5b53ac0b9..f2f024e71 100644
--- a/helm/papers/matita/matita.bib
+++ b/helm/papers/matita/matita.bib
@@ -912,6 +912,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",
@@ -938,6 +947,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}",
@@ -976,6 +992,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}",