/me reviewed up to section 2 (included)

[helm.git] / helm / papers / matita / matita2.bbl

diff --git a/helm/papers/matita/matita2.bbl b/helm/papers/matita/matita2.bbl
index 936fd713d5b89f1114ad70cf0ed3d1c3310854f6..865dcc468d80226e826cf57364e2813f1d0a7588 100644 (file)
--- a/helm/papers/matita/matita2.bbl
+++ b/helm/papers/matita/matita2.bbl
@@ -1,5 +1,11 @@
 \begin{thebibliography}{00}
 
+\bibitem{adams}
+Adams, A.~A.: 2003, `Digitisation, Representation and Formalisation: Digital
+  Libraries of Mathematics.'.
+\newblock In: J.~D. A.~Asperti, B.~Buchberger (ed.): {\em Proceedings of
+  Mathematical Knowledge Management 2003}, Vol. LNCS, 2594. pp. 1--16.
+
 \bibitem{mkm-helm}
 Asperti, A., F. Guidi, L. Padovani, C. {Sacerdoti Coen}, and I. Schena: 2003,
   `Mathematical Knowledge Management in {HELM}'.
@@ -34,6 +40,10 @@ Aspinall, D.: 2000, `{P}roof {G}eneral: A Generic Tool for Proof Development'.
 \newblock In: {\em Tools and Algorithms for the Construction and Analysis of
   Systems, TACAS 2000}, Vol. 1785 of {\em LNCS}.
 
+\bibitem{barthe95implicit}
+Barthe, G.: 1995, `Implicit Coercions in Type Systems'.
+\newblock In: {\em {TYPES}}. pp. 1--15.
+
 \bibitem{proof-by-pointing}
 Bertot, Y.: 1993, `Proof by Pointing'.
 \newblock In: {\em Symposium on Theoretical Aspects Computer Software (STACS)},
@@ -64,6 +74,16 @@ Coscoy, Y., G. Kahn, and L. Thery: 1995, `{Extracting Text from Proofs}'.
 \newblock Technical Report RR-2459, Inria (Institut National de Recherche en
   Informatique et en Automatique), France.
 
+\bibitem{lcf}
+Gordon, M. J.~C., R. Milner, and C. Wadsworth: 1979, `{Edinburgh LCF}: a
+  Mechanised Logic of Computation'.
+\newblock In: {\em Lecture Notes in Computer Science}, Vol.~78 of {\em Lecture
+  Notes in Computer Science}.
+
+\bibitem{lego}
+Lego, `The {L}ego proof-assistant'.
+\newblock \\\url{http://www.dcs.ed.ac.uk/home/lego/}.
+
 \bibitem{mathml}
 MathML: 2003, `Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0'.
 \newblock W3C Recommendation 21 February 2001,