helm/papers/matita/matita2.bbl

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