Johannes Hölzl

My interest is formalizing mathematics and verifying software in interactive theorem provers. Since April 2019, I work as a Formal Verification Engineer at Apple.

Google Scholar - ORCID - DBLP - GitHub @johoelzl - Bitbucket @johannes2011 - Twitter @johannes2007

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. From 2013 until January 2017 I was working on the DFG project Ni/491 15-1. From February 2017 to October 2017 I was at CMU's Department of Philosophy with Jeremy Avigad. Working with the Lean Theorem Prover. Afterwards, I joined Jasmin Blanchette's team at the VU. There I worked on Matryoshka and later Lean Forward.

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

Publications

Journal Articles

Conference Proceedings

Workshops

Thesis

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
SEP
Developing Isabelle user interface components for interactive Prover-IDEs based on jEdit. This is the origin of isabelle-jedit.
IDP
Verifying the up-down algorithm