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.
- Isabelle Tutorial at the Workshop on Formal Theorem Proving, Belgrade, Serbia.
Events
- AICA 2016: Industrial Applications of Computer Algebra, 21 June, Logroño, Spain.
- FOMUS: Workshop on the Foundation of Mathematics, 18 – 23 July, Bielefeld, Germany
(slides and exercises).
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 de