helm/papers/matita/matita2.bbl

   1 \begin{thebibliography}{00}
   2
   3 \bibitem{adams}
   4 Adams, A.~A.: 2003, `Digitisation, Representation and Formalisation: Digital
   5   Libraries of Mathematics.'.
   6 \newblock In: J.~D. A.~Asperti, B.~Buchberger (ed.): {\em Proceedings of
   7   Mathematical Knowledge Management 2003}, Vol. LNCS, 2594. pp. 1--16.
   8
   9 \bibitem{mkm-helm}
  10 Asperti, A., F. Guidi, L. Padovani, C. {Sacerdoti Coen}, and I. Schena: 2003,
  11   `Mathematical Knowledge Management in {HELM}'.
  12 \newblock {\em Annals of Mathematics and Artificial Intelligence} {\bf
  13   38(1-3)}, 27--46.
  14
  15 \bibitem{whelp}
  16 Asperti, A., F. Guidi, C. {Sacerdoti Coen}, E. Tassi, and S. Zacchiroli: 2004,
  17   `A content based mathematical search engine: Whelp'.
  18 \newblock In: {\em Post-proceedings of the Types 2004 International
  19   Conference}, Vol. LNCS, 3839. pp. 17--32.
  20
  21 \bibitem{content-centric}
  22 Asperti, A., L. padovani, C. {Sacerdoti Coen}, and irene Schena: 2000,
  23   `Content-centric Logical Envirnoments'.
  24 \newblock Short Presentation at the Fifteenth IEEE Symposium on Logic in
  25   Computer Science.
  26
  27 \bibitem{remathematization}
  28 Asperti, A., L. Padovani, C. {Sacerdoti Coen}, and I. Schena: 2001, `{XML},
  29   Stylesheets and the re-mathematization of Formal Content'.
  30 \newblock In: {\em EXTREME}.
  31
  32 \bibitem{pechino}
  33 Asperti, A. and B. Wegner: 2003, `An Approach to Machine-Understandable
  34   Representation of the Mathematical Information in Digital Documents'.
  35 \newblock In: F. Bai and B. Wegner (eds.): {\em Electronic Information and
  36   Communication in Mathematics}, Vol. LNCS, 2730. pp. 14--23.
  37
  38 \bibitem{proofgeneral}
  39 Aspinall, D.: 2000, `{P}roof {G}eneral: A Generic Tool for Proof Development'.
  40 \newblock In: {\em Tools and Algorithms for the Construction and Analysis of
  41   Systems, TACAS 2000}, Vol. 1785 of {\em LNCS}.
  42
  43 \bibitem{barthe95implicit}
  44 Barthe, G.: 1995, `Implicit Coercions in Type Systems'.
  45 \newblock In: {\em {TYPES}}. pp. 1--15.
  46
  47 \bibitem{proof-by-pointing}
  48 Bertot, Y.: 1993, `Proof by Pointing'.
  49 \newblock In: {\em Symposium on Theoretical Aspects Computer Software (STACS)},
  50   Vol. 789 of {\em Lecture Notes in Computer Science}.
  51
  52 \bibitem{ctcoq1}
  53 Bertot, Y.: 1999, `The CtCoq System: Design and Architecture'.
  54 \newblock {\em Formal Aspects of Computing} {\bf 11}, 225--243.
  55
  56 \bibitem{gdome2}
  57 Casarini, P. and L. Padovani: 2002, `The {G}nome {DOM} {E}ngine'.
  58 \newblock {\em Markup Languages: Theory \& Practice} {\bf 3}(2), 173--190.
  59
  60 \bibitem{nuprl-book}
  61 Constable, R.~L., S.~F. Allen, H.~M. Bromley, W.~R. Cleaveland, J.~F. Cremer,
  62   R.~W. Harper, D.~J. Howe, T.~B. Knoblock, N.~P. Mendler, P. Panangaden, J.~T.
  63   Sasaki, and S.~F. Smith: 1986, {\em Implementing Mathematics with the {N}uprl
  64   Development System}.
  65 \newblock NJ: Prentice-Hall.
  66
  67 \bibitem{YANNTHESIS}
  68 Coscoy, Y.: 2000, `Explication textuelle de preuves pour le {C}alcul des
  69   {C}onstructions {I}nductives'.
  70 \newblock Ph.D. thesis, Universit\'e de Nice-Sophia Antipolis.
  71
  72 \bibitem{natural}
  73 Coscoy, Y., G. Kahn, and L. Thery: 1995, `{Extracting Text from Proofs}'.
  74 \newblock Technical Report RR-2459, Inria (Institut National de Recherche en
  75   Informatique et en Automatique), France.
  76
  77 \bibitem{lcf}
  78 Gordon, M. J.~C., R. Milner, and C. Wadsworth: 1979, `{Edinburgh LCF}: a
  79   Mechanised Logic of Computation'.
  80 \newblock In: {\em Lecture Notes in Computer Science}, Vol.~78 of {\em Lecture
  81   Notes in Computer Science}.
  82
  83 \bibitem{lego}
  84 Lego, `The {L}ego proof-assistant'.
  85 \newblock \\\url{http://www.dcs.ed.ac.uk/home/lego/}.
  86
  87 \bibitem{mathml}
  88 MathML: 2003, `Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0'.
  89 \newblock W3C Recommendation 21 February 2001,
  90   \url{http://www.w3.org/TR/MathML2}.
  91
  92 \bibitem{omdoc}
  93 OMDoc: 2005, `{OMDoc}: An Open Markup Format for Mathematical Documents
  94   (Version 1.1)'.
  95 \newblock \\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}.
  96
  97 \bibitem{padovani}
  98 Padovani, L.: 2003a, `MathML Formatting'.
  99 \newblock Ph.D. thesis, University of Bologna.
 100 \newblock Technical Report UBLCS 2003-03.
 101
 102 \bibitem{latexmathml}
 103 Padovani, L.: 2003b, `On the Roles of LATEX and MathML in Encoding and
 104   Processing Mathematical Expressions'.
 105 \newblock In: {\em MKM '03: Proceedings of the Second International Conference
 106   on Mathematical Knowledge Management}. London, UK, pp. 66--79.
 107
 108 \bibitem{exportation-module}
 109 {Sacerdoti Coen}, C.: 2003, `From Proof-Assistans to Distributed Libraries of
 110   Mathematics: Tips and Pitfalls'.
 111 \newblock In: A. Asperti, B. Buchberger, and J.~H. Davenport (eds.): {\em
 112   Proceedings of the Second International Conference on Mathematical Knowledge
 113   Management, MKM 2003}, Vol. LNCS, 2594. pp. 30--44.
 114
 115 \bibitem{disambiguation}
 116 {Sacerdoti Coen}, C. and S. Zacchiroli: 2004, `Efficient Ambiguous Parsing of
 117   Mathematical Formulae'.
 118 \newblock In: A.~T. Andrea~Asperti, Grzegorz~Bancerek (ed.): {\em Proceedings
 119   of Mathematical Knowledge Management 2004}, Vol. LNCS, 3119. pp. 347--362.
 120
 121 \bibitem{CoqManual}
 122 {The Coq Development Team}: 2005, `The {C}oq Proof Assistant Reference Manual'.
 123 \newblock \\\url{http://coq.inria.fr/doc/main.html}.
 124
 125 \bibitem{Werner}
 126 Werner, B.: 1994, `Une Th\'eorie des {C}onstructions {I}nductives'.
 127 \newblock Ph.D. thesis, Universit\'e Paris VII.
 128
 129 \bibitem{debrujinfactor}
 130 Wiedijk, F.: 2000, `The ``de Bruijn factor'''.
 131 \newblock \\\url{http://www.cs.ru.nl/~freek/factor/}.
 132
 133 \bibitem{zack-master}
 134 Zacchiroli, S.: 2003, `Web {s}ervices per il supporto alla dimostrazione
 135   interattiva'.
 136 \newblock Master's thesis, University of Bologna.
 137
 138 \end{thebibliography}