X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita2.bbl;h=9ccdd2e07bb8c0e8f63584afc43e6d0e99730e65;hb=bee89433d9f3054eca7d6420a8bdcedb3b4e8523;hp=936fd713d5b89f1114ad70cf0ed3d1c3310854f6;hpb=b8f0a76121fe684674c95fe9389b2e60b5eda694;p=helm.git

diff --git a/helm/papers/matita/matita2.bbl b/helm/papers/matita/matita2.bbl
index 936fd713d..9ccdd2e07 100644
--- 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}'.
@@ -21,7 +27,7 @@ Asperti, A., L. padovani, C. {Sacerdoti Coen}, and irene Schena: 2000,
 \bibitem{remathematization}
 Asperti, A., L. Padovani, C. {Sacerdoti Coen}, and I. Schena: 2001, `{XML},
   Stylesheets and the re-mathematization of Formal Content'.
-\newblock In: {\em EXTREME}.
+\newblock In: {\em Electronic Proceedings of {EXTREME Markup Languages} 2001}.
 
 \bibitem{pechino}
 Asperti, A. and B. Wegner: 2003, `An Approach to Machine-Understandable
@@ -34,15 +40,26 @@ 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{proof-by-pointing}
-Bertot, Y.: 1993, `Proof by Pointing'.
-\newblock In: {\em Symposium on Theoretical Aspects Computer Software (STACS)},
-  Vol. 789 of {\em Lecture Notes in Computer Science}.
+\bibitem{barthe95implicit}
+Barthe, G.: 1995, `Implicit Coercions in Type Systems'.
+\newblock In: {\em Types for Proofs and Programs: International Workshop,
+  {TYPES 1995}}. pp. 1--15.
 
 \bibitem{ctcoq1}
 Bertot, Y.: 1999, `The CtCoq System: Design and Architecture'.
 \newblock {\em Formal Aspects of Computing} {\bf 11}, 225--243.
 
+\bibitem{CoqArt}
+Bertot, Y. and P. Castéran: 2004, {\em {Interactive Theorem Proving and
+  Program Development}}, Texts in Theoretical Computer Science.
+\newblock Springer Verlag.
+\newblock ISBN-3-540-20854-2.
+
+\bibitem{proof-by-pointing}
+Bertot, Y., G. Kahn, and L. Th\'ery: 1994, `Proof by Pointing'.
+\newblock In: {\em Symposium on Theoretical Aspects Computer Software (STACS)},
+  Vol. 789 of {\em Lecture Notes in Computer Science}.
+
 \bibitem{gdome2}
 Casarini, P. and L. Padovani: 2002, `The {G}nome {DOM} {E}ngine'.
 \newblock {\em Markup Languages: Theory \& Practice} {\bf 3}(2), 173--190.
@@ -64,15 +81,46 @@ 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{delahaye}
+Delahaye, D. and R. di~Cosmo: 1999, `Information Retrieval in a {C}oq Proof
+  Library using Type Isomorphisms'.
+\newblock In: {\em Proceedings of TYPES 99}, Vol. LNCS.
+
+\bibitem{geuvers-jojgov}
+Geuvers, H. and G.~I. Jojgov: 2002, `Open Proofs and Open Terms: A Basis for
+  Interactive Logic'.
+\newblock In: J. Bradfield (ed.): {\em Computer Science Logic: 16th
+  International Workshop, CLS 2002}, Vol. LNCS, 2471. pp. 537--552.
+
+\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,
   \url{http://www.w3.org/TR/MathML2}.
 
+\bibitem{munoz}
+Munoz, C.: 1997, `A Calculus of Substitutions for Incomplete-Proof
+  Representation in Type Theory'.
+\newblock Ph.D. thesis, INRIA.
+
+\bibitem{paramodulation}
+Nieuwenhuis, R. and A. Rubio: 2001, {\em Paramodulation-based thorem proving}.
+\newblock Elsevier and MIT Press.
+\newblock ISBN-0-262-18223-8.
+
 \bibitem{omdoc}
-OMDoc: 2005, `{OMDoc}: An Open Markup Format for Mathematical Documents
-  (Version 1.1)'.
-\newblock \\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}.
+OMDoc: 2005, `{OMDoc}: An Open Markup Format for Mathematical Documents (Draft,
+  Version 1.2)'.
+\newblock \\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.2.pdf}.
 
 \bibitem{padovani}
 Padovani, L.: 2003a, `MathML Formatting'.
@@ -98,6 +146,10 @@ Padovani, L.: 2003b, `On the Roles of LATEX and MathML in Encoding and
 \newblock In: A.~T. Andrea~Asperti, Grzegorz~Bancerek (ed.): {\em Proceedings
   of Mathematical Knowledge Management 2004}, Vol. LNCS, 3119. pp. 347--362.
 
+\bibitem{strecker}
+Strecker, M.: 1998, `Construction and Deduction in Type Theories'.
+\newblock Ph.D. thesis, Universit{\"a}t Ulm.
+
 \bibitem{CoqManual}
 {The Coq Development Team}: 2005, `The {C}oq Proof Assistant Reference Manual'.
 \newblock \\\url{http://coq.inria.fr/doc/main.html}.