Hello

My research interests lie in the Formalisation of Mathematics in Theorem Provers. I focus on the following topics:

• Locales: Isabelle's module system
• Formalisation of mathematics in Higher-Order Logic and Set Theory
  • Take a look at the algebra library formalised in Isabelle-HOL!
• Interfaces for reasoning components

Events

• Introduction to the Isabelle Proof Assistant: 29 January – 1 February 2008, Belgrade, Serbia.
• LSFA '08: Workshop on Logical and Semantic Frameworks, 26 August 2008, Salvador, Brazil.

Downloads

• Corpus of parametric linear equation systems.
• Theory of abstract algebra for Isabelle/HOL (part of the distribution).
• Working with the repository version of Isabelle (only useful for developers).
• Slides and exercises for the Isabelle Tutorial at IJCAR 2004.

Contact

Telephone: +43-512-507-6437
Fax: +43-512-507-9887
Location: room 3N07 in the ICT building

E-mail: clemens ballarin (at) uibk ac at