| Opening |
Cohen |
| Short Presentations |
Viglione |
How to achieve
user-friendly interactivity in mathematical exercises on the Web
|
PDF and
HTML
|
| Lavirotte |
Plan for a mathematical content editor based on SVG display |
PDF
|
| Kohlhase |
Towards a Mizar Mathematical Library in OMDoc format |
PDF
|
| Sexton |
Glyph recognition for optical mathematical text capture |
| Invited Lectures |
Newhouse |
Grid Services |
PDF
|
| Nederpelt |
Formalizing Mathematics in the Automath Tradition |
HTML
|
| Linton |
Interfacing with GAP |
PDF |
| MKM |
Session Chair: Davenport |
| Davenport |
MKM Overview |
| Dewar |
Semantic Markup for Legacy Documents |
HTML
|
| Rioboo |
The Foc Project |
| Autexier |
Management of Change in MAYA |
PDF
|
| Libbrecht |
Authoring semantic mathematical documents with
QMath and OQMath
|
HTML
|
| Libbrecht |
ActiveMath: Latest Developments Update |
HTML
|
| MoWGLI |
Session Chair: Asperti |
| Sacerdoti Coen |
XML encoding and transformation of the Coq library |
| Padovani |
The GTK Mathview widget |
PDF
|
| Bertot |
Mathematical Interfaces |
HTML
|
| Goguadze |
Metadata for mathematical documents |
| CALCULEMUS |
Session Chair: Benzmüller |
| Benzmüller |
The CALCULEMUS Network — A brief Introduction |
PDF
|
| Cohen / Sorge |
Groups and Certificates |
PDF
|
| Trybulec |
The evolution of the Mizar Mathematical Library |
PDF
|
| Zimmer |
The MathWeb Software Bus and Theorem Proving Services |
| TYPES |
Session Chair: Geuvers |
| Geuvers |
The use of types to formalize mathematics |
| Luo |
The type-theoretic approach to mathematical vernacular |
HTML
|
| Bertot |
Types for Proofs, Computers and Mathematics |
PDF
|
| Ballarin |
Isabelle/Isar: formal, yet human-readable proof documents |
PDF
|
| MONET |
Session Chair: Dewar |
| Dewar |
The MONET Project |
HTML
|
| Chicha / Gaëtano |
Putting Bernina on the Web |
PDF
|
| Caprotti |
The Mathematical Service Description Language |
| Horrocks |
OWL: an Ontology Language for the Semantic Web |
PDF
|
| OpenMath |
Session Chair: Cohen |
| Hagen |
XML, TeX and Math |
| Reinaldo Barreiro |
Context in Interactive Mathematical Documents |
| Kohlhase |
Towards OpenMath version 2 |
PDF
|