Next: Chalmers
Up: Cooperating sites
Previous: Birmingham


The Helm group (Hypertextual Electronic Library of Mathematics) is active in Bologna since 1999. The work of the group has been mainly focused on the application of information technologies (e.g. XML) to the problems of management and (web) publishing of large repositories of formal mathematical knowledge.

We are coordinating the European FET-open Project IST-2001-33562 MoWGLI (, which includes the TYPES sites at Sophia-Antipolis, Nijmegen and Trusted Logic. We recently organized and chaired the Second International Conference on Mathemtical Knowledge Management, in Bertinoro Italy (February 2003). We are also developing our own proof assistant (a clone of Coq), where the several components are all centered around and communicate through the XML low-level encoding of the mathematical entities.

Our main contribution to the TYPES project will be in the area of formalisation of mathematics, focussing on intefaces and tools for the automation of formal reasoning, and the management "in the large" of mathematical information. Our work is integrated with the Coq proof tool, and we plan to apply our approach with other TYPES proof tools.

The senior members of the Helm Group are

Bologna homepage

Bengt Nordström 2005-09-22