Johannes Hölzl

Johannes Hölzl

Post-doctoral Researcher, Faculty of Science — Computer Science, Vrije Universiteit Amsterdam

Contact

dr. J. Hölzl
W & N Building, Room T-443
Vrije Universiteit Amsterdam
Department of Computer Science
Section of Theoretical Computer Science
De Boelelaan 1081a
1081 HV Amsterdam
The Netherlands

Selected Publications


A formally verified proof of the Central Limit Theorem

Jeremy Avigad Johannes Hölzl Luke Serafin
J. Autom. Reasoning 59(4) (pages 389-423)
The final publication is available at Springer Link.


Markov Chains and Markov Decision Processes in Isabelle/HOL

Johannes Hölzl
J. Autom. Reasoning 59(3) (pages 345-387)
The final publication is available at Springer Link.


Type Classes and Filters for Mathematical Analysis in Isabelle/HOL

Johannes Hölzl Fabian Immler Brian Huffman
ITP 2013 (pages 279-294)
The final publication is available at Springer Link.


Publications

A formally verified proof of the Central Limit Theorem

Jeremy Avigad Johannes Hölzl Luke Serafin
J. Autom. Reasoning 59(4) (pages 389-423)
The final publication is available at Springer Link.


Markov Chains and Markov Decision Processes in Isabelle/HOL

Johannes Hölzl
J. Autom. Reasoning 59(3) (pages 345-387)
The final publication is available at Springer Link.


Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Jasmin Christian Blanchette Aymeric Bouzy Martin Desharnais Mathias Fleury Johannes Hölzl Ondřej Kunčar Andreas Lochbihler Fabian Meier Lorenz Panny Andrei Popescu Christian Sternagel René Thiemann Dmitriy Traytel
FroCoS 2017 (pages 3-21)


Verification of the UpDown Scheme

Johannes Hölzl

AFP

Type Classes and Filters for Mathematical Analysis in Isabelle/HOL

Johannes Hölzl Fabian Immler Brian Huffman
ITP 2013 (pages 279-294)
The final publication is available at Springer Link.


Three Chapters of Measure Theory in Isabelle/HOL

Johannes Hölzl Armin Heller
ITP 2011 (pages 135-151)
The final publication is available at Springer Link.


Specifying and verifying sparse matrix codes

Gilad Arnold Johannes Hölzl Ali Sinan Köksal Mooly Sagiv
ICFP 2010 (pages 249-260)