+++ /dev/null
-\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}'.
-\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, 3839. pp. 17--32.
-
-\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 Electronic Proceedings of {EXTREME Markup Languages} 2001}.
-
-\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{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.
-
-\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{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 (Draft,
- Version 1.2)'.
-\newblock \\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.2.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{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}.
-
-\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}
projects / helm.git / blobdiff