+\begin{thebibliography}{00}
+
+\bibitem{mkm-helm}
+Asperti, A., F. Guidi, L. Padovani, C. {Sacerdoti Coen}, and I. Schena: 2003,
+ `Mathematical Knowledge Management in {HELM}'.
+\newblock {\em Annals of Mathematics and Artificial Intelligence} {\bf
+ 38(1-3)}, 27--46.
+
+\bibitem{whelp}
+Asperti, A., F. Guidi, C. {Sacerdoti Coen}, E. Tassi, and S. Zacchiroli: 2004,
+ `A content based mathematical search engine: Whelp'.
+\newblock In: {\em Post-proceedings of the Types 2004 International
+ Conference}, Vol. LNCS, (to appear). pp. xxx--xxx.
+
+\bibitem{content-centric}
+Asperti, A., L. padovani, C. {Sacerdoti Coen}, and irene Schena: 2000,
+ `Content-centric Logical Envirnoments'.
+\newblock Short Presentation at the Fifteenth IEEE Symposium on Logic in
+ Computer Science.
+
+\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}.
+
+\bibitem{pechino}
+Asperti, A. and B. Wegner: 2003, `An Approach to Machine-Understandable
+ Representation of the Mathematical Information in Digital Documents'.
+\newblock In: F. Bai and B. Wegner (eds.): {\em Electronic Information and
+ Communication in Mathematics}, Vol. LNCS, 2730. pp. 14--23.
+
+\bibitem{proofgeneral}
+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{ctcoq1}
+Bertot, Y.: 1999, `The CtCoq System: Design and Architecture'.
+\newblock {\em Formal Aspects of Computing} {\bf 11}, 225--243.
+
+\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.
+
+\bibitem{nuprl-book}
+Constable, R.~L., S.~F. Allen, H.~M. Bromley, W.~R. Cleaveland, J.~F. Cremer,
+ R.~W. Harper, D.~J. Howe, T.~B. Knoblock, N.~P. Mendler, P. Panangaden, J.~T.
+ Sasaki, and S.~F. Smith: 1986, {\em Implementing Mathematics with the {N}uprl
+ Development System}.
+\newblock NJ: Prentice-Hall.
+
+\bibitem{YANNTHESIS}
+Coscoy, Y.: 2000, `Explication textuelle de preuves pour le {C}alcul des
+ {C}onstructions {I}nductives'.
+\newblock Ph.D. thesis, Universit\'e de Nice-Sophia Antipolis.
+
+\bibitem{natural}
+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{mathml}
+Mathematical: 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{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}.
+
+\bibitem{padovani}
+Padovani, L.: 2003a, `MathML Formatting'.
+\newblock Ph.D. thesis, University of Bologna.
+\newblock Technical Report UBLCS 2003-03.
+
+\bibitem{latexmathml}
+Padovani, L.: 2003b, `On the Roles of LATEX and MathML in Encoding and
+ Processing Mathematical Expressions'.
+\newblock In: {\em MKM '03: Proceedings of the Second International Conference
+ on Mathematical Knowledge Management}. London, UK, pp. 66--79.
+
+\bibitem{exportation-module}
+{Sacerdoti Coen}, C.: 2003, `From Proof-Assistans to Distributed Libraries of
+ Mathematics: Tips and Pitfalls'.
+\newblock In: A. Asperti, B. Buchberger, and J.~H. Davenport (eds.): {\em
+ Proceedings of the Second International Conference on Mathematical Knowledge
+ Management, MKM 2003}, Vol. LNCS, 2594. pp. 30--44.
+
+\bibitem{disambiguation}
+{Sacerdoti Coen}, C. and S. Zacchiroli: 2004, `Efficient Ambiguous Parsing of
+ Mathematical Formulae'.
+\newblock In: A.~T. Andrea~Asperti, Grzegorz~Bancerek (ed.): {\em Proceedings
+ of Mathematical Knowledge Management 2004}, Vol. LNCS, 3119. pp. 347--362.
+
+\bibitem{CoqManual}
+Team, T. C.~D.: 2005, `The {C}oq Proof Assistant Reference Manual'.
+\newblock \\\url{http://coq.inria.fr/doc/main.html}.
+
+\bibitem{Werner}
+Werner, B.: 1994, `Une Th\'eorie des {C}onstructions {I}nductives'.
+\newblock Ph.D. thesis, Universit\'e Paris VII.
+
+\bibitem{debrujinfactor}
+Wiedijk, F.: 2000, `The ``de Bruijn factor'''.
+\newblock \\\url{http://www.cs.ru.nl/~freek/factor/}.
+
+\bibitem{zack-master}
+Zacchiroli, S.: 2003, `Web {s}ervices per il supporto alla dimostrazione
+ interattiva'.
+\newblock Master's thesis, University of Bologna.
+
+\end{thebibliography}