Bibliography

1. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
   Content-centric Logical Environments.
   Short Presentation at LICS-2000.
   Abstract: There is a compelling need of integration between the current tools for automation of formal reasoning and mechanization of mathematics (proof assistants and logical frameworks) and the most recent technologies for the development of web applications and electronic publishing. Currently, libraries in logical frameworks are usually saved in two formats: a textual one, in the specific tactical language of the proof assistant, and a compiled (proof checked) one in some internal, concrete representation language. Both representations are obviously unsatisfactory, since they are too oriented to the specific application: the information is not directly available, if not by means of the functionalities offered by the system itself. This is in clear contrast with the main guidelines of the modern Information Society, and its new emphasis on content.
   
   
2. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
   Towards a Library of Formal Mathematics.
   Short presentation at TPHOLS2000.
   Abstract: The eXtensible Markup Language (XML) opens the possibility to start anew, on a solid technological ground, the ambitious goal of developing a suitable technology for the creation and maintenance of a virtual, distributed, hypertextual library of formal mathematical knowledge. In particular, XML provides a central technology for storing, retrieving and processing mathematical documents, comprising sophisticated web-publishing mechanisms (stylesheets) covering notational and stylistic issues. In this paper, we discuss the overall architectural design of the new systems, and our progress in this direction.
   
   
3. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
   Formal Mathematics on the Web.
   Presentation at Crimea 2001.
   Abstract: not available
   
   
4. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
   HELM and the Semantic Math-Web.
   To appear in Proc. of TPHOLS 2001, Springer-Verlag, Lectures Notes in Computer Science (LNCS) Series.
   Abstract: The eXtensible Markup Language (XML) opens the possibility to start anew, on a solid technological ground, the ambitious goal of developing a suitable technology for the creation and maintenance of a virtual, distributed, hypertextual library of formal mathematical knowledge. In particular, XML provides a central technology for storing, retrieving and processing mathematical documents, comprising sophisticated web-publishing mechanisms (stylesheets) covering notational and stylistic issues. By the application of XML technology to the large repositories of structured, content oriented information offered by Logical Frameworks we meet the ultimate goal of the Semantic Web, that is to allow machines the sharing and exploitation of knowledge in the Web way, i.e. without central authority, with few basic rules, in a scalable, adaptable, extensible manner.
   
   
5. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
   XML, Stylesheets and the re-mathematization of Formal Content.
   To appear in Proc. of EXTREME 2001.
   Abstract: An important part of the descriptive power of mathematics derives from its ability to represent formal concepts in a highly evolved, two-dimensional system of symbolic notations. Tools for the mechanisation of mathematics and the automation of formal reasoning must eventually face the problem of re-mathematization of the logical, symbolic content of the information, especially in view of their integration with the World Wide Web. In a different work, we already discussed the pivotal role that XML technology is likely to play in such an integration. In this paper, we focus on the problem of (Web) publishing, advocating the use of XSL Transformations, in conjunction with MathML, as a standard, application independent and modular way for associating notation to formal mathematical content.
   
   
6. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
   Formal Mathematics in MathML.   HTML Version   Slides
   Presentation at the MathML International Conference 2000.
   Abstract: not available
   
   
7. C. Sacerdoti Coen.
   Progettazione e realizzazione con tecnologia XML di basi distribuite di conoscenza matematica formalizzata.
   Master thesis (Italian version only).
   Also available as [HTML version] e [HTML version (single page)]
   Abstract: Fully describes the status of project HELM and the design and implementation choises taken from its birth to autumn 2000.