Project HELM: an Hypertextual Electronic Library of Mathematic
Claudio Sacerdoti
University of Bologna
Abstract:
I will briefly present the aims and the general architecture of project HELM
and I will describe the tools already developed. In particular, I
will describe a module to export CIC objects to XML, an incremental
type-checker for them based on a new notion of environment, the model
of distribution for the library files and the related tools and a
stylesheet architecture to render the XML objects applying both
ad-hoc and general mathematical notation and natural language synthesis.
Using the previous tools as an instrument to inspect lambda-terms
reveals that many of the tactics of Coq are implemented in a
poor-way. I will give some examples of this and then I will briefly
sketch some ideas on tactic metrics definition and I will discuss
a (concrete) example of tactic improvement (in the sense of
term-size, retyping time and proof ``naturality'').
Back to schedule.
Marieke Huisman