I'm currently at CMU's Department of Philosophy with Jeremy Avigad. Working with the Lean Theorem Prover.
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 151. Since February 2017 I'm at CMU.
My interest is mostly formalizing mathematics in interactive theorem provers. I'm currently working on basic automation and library for Lean. I worked in Isabelle's higherorder logic, worked on its analysis, developed its measure and probability theory, and used this to verify probabilistic software.
Wir müssen wissen,
wir werden wissen.

David Hilbert
Publications
Journal Articles
 A formally verified proof of the Central Limit Theorem (Preprint).
Jeremy Avigad, Johannes Hölzl, and Luke Serafin.
Submitted for review to the Journal of Automated Reasoning. arxiv (1405.7012)  Markov chains and Markov decision processes in Isabelle/HOL (Preprint).
Johannes Hölzl.
Accepted for publication in the Journal of Automated Reasoning. BibTex Slides
(The original publication is available at Springer Link)  Formal Verification of LanguageBased Concurrent Noninterference.
Andrei Popescu, Johannes Hölzl, and Tobias Nipkow.
Journal of Formalized Reasoning 6(1), 2013. BibTex
Conference Proceedings
 Markov Processes in Isabelle/HOL.
Johannes Hölzl.
Proceedings of CPP '17. BibTex
©Johannes Hölzl 2017. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive version was published in the proceedings of CPP 2017.  Formalising Semantics for Expected Running Time of Probabilistic Programs (Rough Diamond).
Johannes Hölzl.
Proceedings of ITP '16. BibTex Slides
(The original publication is available at Springer Link)  A Formalized Hierarchy of Probabilistic System Types  Proof Pearl.
Johannes Hölzl, Andreas Lochbihler, and Dmitriy Traytel.
Proceedings of ITP '15 (LNCS 9236). BibTex Slides
(The original publication is available at Springer Link)  A Verified Compiler for Probability Density Functions.
Manuel Eberl, Johannes Hölzl, and Tobias Nipkow.
Proceedings of ESOP '15. (LNCS 9032) BibTex
(The original publication is available at Springer Link)  Recursive Functions on Lazy Lists via Domains and Topologies.
Andreas Lochbihler and Johannes Hölzl.
Proceedings of ITP '14 (LNCS 8558). BibTex
(The original publication is available at Springer Link)  Truly Modular (Co)datatypes for Isabelle/HOL.
Jasmin C. Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel.
Proceedings of ITP '14 (LNCS 8558). BibTex
(The original publication is available at Springer Link)  Formalizing Probabilistic Noninterference.
Andrei Popescu, Johannes Hölzl, and Tobias Nipkow.
Proceedings of CPP 2013 (LNCS 8307). BibTex
(The original publication is available at Springer Link)  Noninterfering Schedulers  When Possibilistic Noninterference Implies Probabilistic Noninterference.
Andrei Popescu, Johannes Hölzl, and Tobias Nipkow.
Proceedings of CALCO 2013 (LNCS 8089). BibTex
(The original publication is available at Springer Link)  Type Classes and Filters for Mathematical Analysis in Isabelle/HOL.
Johannes Hölzl, Fabian Immler, and Brian Huffman.
Proceedings of ITP '13 (LNCS 7998). BibTex
(The original publication is available at Springer Link)  Proving concurrent noninterference.
Andrei Popescu, Johannes Hölzl, and Tobias Nipkow.
Proceedings of CPP '12 (LNCS 7679). BibTex
(The original publication is available at Springer Link)  Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL.
Fabian Immler and Johannes Hölzl.
Proceedings of ITP '12 (LNCS 7406). BibTex
(The original publication is available at Springer Link)  Verifying pCTL Model Checking.
Johannes Hölzl and Tobias Nipkow.
Proceedings of TACAS '12 (LNCS 7214). BibTex
(The original publication is available at Springer Link)  Three Chapters of Measure Theory.
Johannes Hölzl and Armin Heller.
Proceedings of ITP '11 (LNCS 6898). BibTex
(The original publication is available at Springer Link)  Specifying and
Verifying Sparse Matrix Codes.
Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, and Mooly Sagiv.
Proceedings of ICFP '10. (© ACM) BibTex  Proving Inequalities over Reals with Computation
in Isabelle/HOL.
Johannes Hölzl.
Proceedings of PLMMS '09. (© ACM) Slides BibTex
Workshops
 Fixed Points for Markov Decision Processes.
Johannes Hölzl.
Poster presentation at the Workshop on Probabilistic Programming Semantics (PPS2016)  A formally verified proof of the Central Limit Theorem.
Jeremy Avigad, Johannes Hölzl and Luke Serafin.
Published at arXiv. Presented at the Isabelle Workshop 2014. bibTex  Interactive verification of Markov chains: Two distributed protocol case studies.
Johannes Hölzl and Tobias Nipkow.
Proceedings of QFM '12 (EPTCS 103). Slides bibTex
Thesis

Construction and Stochastic Applications of Measure Spaces in HigherOrder Logic.
Institut für Informatik, TU München. October 2012. BibTex
Diploma thesis

Proving RealValued Inequalities by Computation
in Isabelle/HOL.
Diploma thesis. Institut für Informatik, TU München. April 2009. BibTex
Current Work
 Verification of probabilistic models in the interactive theorem prover Isabelle/HOL
 I'm working on the DFG project Ni 491/151 and Ni 491/161.
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 updown algorithm.
 Verification of Sparse Matrix codes
 Gilad Arnold and I are working on automatically verifying the correctness of Sparse Matrix codes.
 Diploma thesis
 Proving RealValued Inequalities by Computation in Isabelle/HOL
 SEP
 Developing Isabelle user interface components for interactive ProverIDEs based on jEdit. This is the origin of isabellejedit.
 IDP
 Verifying the updown algorithm