TUMMy 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
IsabelleI 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.



  • 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
Boltzmannstr. 3
85748 Garching, Germany

Telephone: +49-89-289-17326
Fax: +49-89-289-17307
Location: room 01.11.061 in the FMI building


ballarin at in tum de

Copyright © 2001–2016 by Clemens Ballarin
Last updated 19 July 2016