Personal information

Germany

Biography

I'm not in academia anymore.

I was working on formalizing mathematics in interactive theorem provers. I worked with Isabelle (http://isabelle.in.tum.de/) and Lean (http://leanprover.github.io/).

Activities

Employment (3)

Vrije Universiteit Amsterdam: Amsterdam, Noord-Holland, NL

2017-11 to 2019-03-31 | Researcher (Department of Computer Science)
Employment
Source: Self-asserted source
Johannes Hölzl

Carnegie Mellon University: Pittsburgh, PA, US

2017-02 to 2017-09 | Researcher (Department of Philospohy)
Employment
Source: Self-asserted source
Johannes Hölzl

Technische Universität München: Munchen, Bayern, DE

2009 to 2017-01 | Researcher (Department of Informatics)
Employment
Source: Self-asserted source
Johannes Hölzl

Education and qualifications (2)

Technische Universität München: Munchen, Bayern, DE

2009 to 2013 | Dr. rer. nat. (Department of Informatics)
Education
Source: Self-asserted source
Johannes Hölzl

Technische Universität München: Munchen, Bayern, DE

2004 to 2009 | Diploma (Department of Informatics)
Education
Source: Self-asserted source
Johannes Hölzl

Works (21)

Markov chains and Markov decision processes in Isabelle/HOL

Journal of Automated Reasoning
2017 | Journal article
Source: Self-asserted source
Johannes Hölzl

Markov Processes in Isabelle/HOL

Certified Programs and Proofs (CPP 2017)
2017 | Conference paper
Source: Self-asserted source
Johannes Hölzl

A Verified Compiler for Probability Density Functions

Source: Self-asserted source
Johannes Hölzl
grade
Preferred source (of 2)‎

Formalising Semantics for Expected Running Time of Probabilistic Programs

Interactive Theorem Proving (ITP 2016)
2016 | Conference paper
Source: Self-asserted source
Johannes Hölzl

A Formalized Hierarchy of Probabilistic System Types - Proof Pearl

Interactive Theorem Proving (ITP 2015)
2015 | Conference paper
Source: Self-asserted source
Johannes Hölzl

Recursive Functions on Lazy Lists via Domains and Topologies

Interactive Theorem Proving (ITP 2014)
2014 | Conference paper
Source: Self-asserted source
Johannes Hölzl

Truly modular (co)datatypes for Isabelle/HOL

Interactive Theorem Proving (ITP 2014)
2014 | Conference paper
Source: Self-asserted source
Johannes Hölzl

A formally verified proof of the Central Limit Theorem

2014-05-27 | Preprint
Source: Self-asserted source
Johannes Hölzl

Formal Verification of Language-Based Concurrent Noninterference

Journal of Formalized Reasoning
2013 | Journal article
Source: Self-asserted source
Johannes Hölzl

Formalizing Probabilistic Noninterference

Certified Programs and Proofs (CPP 2013)
2013 | Conference paper
Source: Self-asserted source
Johannes Hölzl

Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference

Algebra and Coalgebra in Computer Science (CALCO 2013)
2013 | Conference paper
Source: Self-asserted source
Johannes Hölzl

Type Classes and Filters for Mathematical Analysis in Isabelle/HOL

Interactive Theorem Proving (ITP 2013)
2013 | Journal article
Part of ISBN: 978-3-642-39633-5
Source: Self-asserted source
Johannes Hölzl

Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic

2012 | Dissertation or Thesis
Source: Self-asserted source
Johannes Hölzl

Interactive verification of Markov chains: Two distributed protocol case studies

Quantities in Formal Methods (QFM 2012)
2012 | Conference paper
Source: Self-asserted source
Johannes Hölzl

Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL

Interactive Theorem Proving (ITP2012)
2012 | Book chapter
Source: Self-asserted source
Johannes Hölzl

Proving Concurrent Noninterference

Certified Programs and Proofs (CPP 2012)
2012 | Book chapter
Source: Self-asserted source
Johannes Hölzl

Verifying pCTL Model Checking

Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)
2012 | Conference paper
Source: Self-asserted source
Johannes Hölzl

Three Chapters of Measure Theory in Isabelle/HOL

Interactive Theorem Proving (ITP 2011)
2011 | Conference paper
Source: Self-asserted source
Johannes Hölzl

Specifying and verifying sparse matrix codes

Proceedings of the 15th ACM SIGPLAN international conference on Functional programming
2010 | Conference paper
Source: Self-asserted source
Johannes Hölzl

Proving Inequalities over Reals with Computation in Isabelle/HOL

Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS'09)
2009 | Conference paper
Source: Self-asserted source
Johannes Hölzl

Proving Real-Valued Inequalities by Computation in Isabelle/HOL

2009 | Supervised student publication
Source: Self-asserted source
Johannes Hölzl