Hello!
My research interests lie in the Formalisation of
Mathematics in Theorem Provers. For an introduction to this field see
my research
page in Innsbruck. I focus
on the following topics:
- Locales: Isabelle's module system
- Formalisation of mathematics in logic
- Interfaces for reasoning components
I
am using the prover Isabelle
for
my research. More information on my work is available. See my list of publications.
Pointers that are relevant to my work can be found among my bookmarks. Downloads
- Corpus of parametric linear equation systems.
- The theory of polynomials has become part of the standard distribution of Isabelle/HOL.
- Working with the repository version of Isabelle (only useful for developers).
- Slides and exercises for the Isabelle Tutorial at IJCAR 2004.
Events
- Introduction to the Isabelle Proof Assistant: 29 January – 1 February, Belgrade, Serbia.
- LSFA '08: Workshop on Logical and Semantic Frameworks, 26 August, Salvador, Brazil.
Teaching
Links about my lectures and projects for students are available on a separate page (in German).My address at work:
Dr. Clemens BallarinInstitut für Informatik
Technische Universität München
Boltzmannstr. 3
85748 Garching, Germany
Telephone: +49-89-289-17326
Fax: +49-89-289-17307
Location: room 01.11.061
in the FMI building
E-mail:
ballarin at in tum deInnsbruck
I also hold a professorship (part-time) at the Universität Innsbruck.