My research interests lie in the Formalisation of
Mathematics in Theorem Provers. For an introduction to this field see
page in Innsbruck. I focus
on the following topics:
am using the prover Isabelle
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.
- Locales: Isabelle's module system
- Formalisation of mathematics in logic
- Interfaces for reasoning components
- 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).
Links about my lectures and projects for students are available on a separate
page (in German).
My address at work:
Dr. Clemens Ballarin
Institut für Informatik
Technische Universität München
85748 Garching, Germany
Location: room 01.11.061
in the FMI building
ballarin at in tum de