1 \begin{thebibliography}{00}
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
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, (to appear). pp. xxx--xxx.
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
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}.
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.
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}.
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}.
43 Bertot, Y.: 1999, `The CtCoq System: Design and Architecture'.
44 \newblock {\em Formal Aspects of Computing} {\bf 11}, 225--243.
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.
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
55 \newblock NJ: Prentice-Hall.
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.
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.
68 Mathematical: 2003, `Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion
70 \newblock W3C Recommendation 21 February 2001,
71 \url{http://www.w3.org/TR/MathML2}.
74 OMDoc: 2005, `{OMDoc}: An Open Markup Format for Mathematical Documents
76 \newblock \\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}.
79 Padovani, L.: 2003a, `MathML Formatting'.
80 \newblock Ph.D. thesis, University of Bologna.
81 \newblock Technical Report UBLCS 2003-03.
84 Padovani, L.: 2003b, `On the Roles of LATEX and MathML in Encoding and
85 Processing Mathematical Expressions'.
86 \newblock In: {\em MKM '03: Proceedings of the Second International Conference
87 on Mathematical Knowledge Management}. London, UK, pp. 66--79.
89 \bibitem{exportation-module}
90 {Sacerdoti Coen}, C.: 2003, `From Proof-Assistans to Distributed Libraries of
91 Mathematics: Tips and Pitfalls'.
92 \newblock In: A. Asperti, B. Buchberger, and J.~H. Davenport (eds.): {\em
93 Proceedings of the Second International Conference on Mathematical Knowledge
94 Management, MKM 2003}, Vol. LNCS, 2594. pp. 30--44.
96 \bibitem{disambiguation}
97 {Sacerdoti Coen}, C. and S. Zacchiroli: 2004, `Efficient Ambiguous Parsing of
98 Mathematical Formulae'.
99 \newblock In: A.~T. Andrea~Asperti, Grzegorz~Bancerek (ed.): {\em Proceedings
100 of Mathematical Knowledge Management 2004}, Vol. LNCS, 3119. pp. 347--362.
103 Team, T. C.~D.: 2005, `The {C}oq Proof Assistant Reference Manual'.
104 \newblock \\\url{http://coq.inria.fr/doc/main.html}.
107 Werner, B.: 1994, `Une Th\'eorie des {C}onstructions {I}nductives'.
108 \newblock Ph.D. thesis, Universit\'e Paris VII.
110 \bibitem{debrujinfactor}
111 Wiedijk, F.: 2000, `The ``de Bruijn factor'''.
112 \newblock \\\url{http://www.cs.ru.nl/~freek/factor/}.
114 \bibitem{zack-master}
115 Zacchiroli, S.: 2003, `Web {s}ervices per il supporto alla dimostrazione
117 \newblock Master's thesis, University of Bologna.
119 \end{thebibliography}