Johannes Hölzl

I studied computer science, with mathematics as minor subject, at the TU München since 2004. From May 2009 until October 2012 I was a graduate student as part of the PUMA graduate school. Since 2013 I'm working on the DFG project Ni/491 15-1 .

Address [vCard]: Dr. Johannes Hölzl
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
85748 Garching
Telephone: +49 (89) 289-17865
Telefax: +49 (89) 289-17307
Office: MI 00.09.051[MI 00.09.051]

My interests are mainly formalizing mathematics in higher-order logic and verifying software upon this. My current work mostly is related to the Isabelle theorem prover.

Wir müssen wissen,
wir werden wissen. - David Hilbert


Journal Articles

Conference Proceedings



Diploma thesis

Current Work

Verification of probabilistic models in the interactive theorem prover Isabelle/HOL
I'm working on the DFG project Ni 491/15-1 and Ni 491/16-1.

Past Work

Measure, Probability, and Information
Together with Armin Heller I formalized the first three chapters of Heinz Bauer's textbook about measure theory. This is now officially part of the Isabelle repository. We built on the work from Aaron Coble which was ported to Isabelle by Lawrence C. Paulson. This work is now largely rewritten and extended, for an overview see my thesis and the work on the Giry monad, on Markov models, on the central limit theorem (CTL), and on Markov processes.
Multivariate Analysis
Robert Himmelmann ported large parts of the formalization of Multivariate Analysis available in HOL Light. The current development is found in the Isabelle repository.
Up Down
I'm working together with Dirk Pflüger on the publication of the verification of the up-down algorithm.
Verification of Sparse Matrix codes
Gilad Arnold and I are working on automatically verifying the correctness of Sparse Matrix codes.
Diploma thesis
Proving Real-Valued Inequalities by Computation in Isabelle/HOL
Developing Isabelle user interface components for interactive Prover-IDEs based on jEdit. This is the origin of isabelle-jedit.
Verifying the up-down algorithm