Follow
Johannes Hölzl
Johannes Hölzl
Vrije Universitet Amsterdam
Verified email at in.tum.de - Homepage
Title
Cited by
Cited by
Year
Truly modular (co) datatypes for Isabelle/HOL
JC Blanchette, J Hölzl, A Lochbihler, L Panny, A Popescu, D Traytel
International Conference on Interactive Theorem Proving, 93-110, 2014
1152014
Type classes and filters for mathematical analysis in Isabelle/HOL
J Hölzl, F Immler, B Huffman
International Conference on Interactive Theorem Proving, 279-294, 2013
1012013
Three chapters of measure theory in Isabelle/HOL
J Hölzl, A Heller
International Conference on Interactive Theorem Proving, 135-151, 2011
942011
Numerical analysis of ordinary differential equations in Isabelle/HOL
F Immler, J Hölzl
International Conference on Interactive Theorem Proving, 377-392, 2012
632012
A formally verified proof of the central limit theorem
J Avigad, J Hölzl, L Serafin
Journal of Automated Reasoning 59 (4), 389-423, 2017
422017
Proving inequalities over reals with computation in Isabelle/HOL
J Hölzl
International Workshop on Programming Languages for Mechanized Mathematics …, 2009
382009
Construction and stochastic applications of measure spaces in higher-order logic
J Hölzl
Technische Universität München, 2013
302013
Specifying and verifying sparse matrix codes
G Arnold, J Hölzl, AS Köksal, R Bodík, M Sagiv
ACM Sigplan Notices 45 (9), 249-260, 2010
262010
A verified compiler for probability density functions
M Eberl, J Hölzl, T Nipkow
European Symposium on Programming Languages and Systems, 80-104, 2015
242015
Markov chains and Markov decision processes in Isabelle/HOL
J Hölzl
Journal of Automated Reasoning 59 (3), 345-387, 2017
232017
Proving concurrent noninterference
A Popescu, J Hölzl, T Nipkow
International Conference on Certified Programs and Proofs, 109-125, 2012
222012
Foundational (co) datatypes and (co) recursion for higher-order logic
J Biendarra, JC Blanchette, A Bouzy, M Desharnais, M Fleury, J Hölzl, ...
International Symposium on Frontiers of Combining Systems, 3-21, 2017
172017
A formalized hierarchy of probabilistic system types
J Hölzl, A Lochbihler, D Traytel
International Conference on Interactive Theorem Proving, 203-220, 2015
162015
Verifying pCTL model checking
J Hölzl, T Nipkow
International Conference on Tools and Algorithms for the Construction and …, 2012
162012
Formalising semantics for expected running time of probabilistic programs
J Hölzl
International Conference on Interactive Theorem Proving, 475-482, 2016
152016
Formalizing probabilistic noninterference
A Popescu, J Hölzl, T Nipkow
International Conference on Certified Programs and Proofs, 259-275, 2013
152013
Recursive functions on lazy lists via domains and topologies
A Lochbihler, J Hölzl
International Conference on Interactive Theorem Proving, 341-357, 2014
142014
Formalizing the solution to the cap set problem
SR Dahmen, J Hölzl, RY Lewis
arXiv preprint arXiv:1907.01449, 2019
132019
Markov processes in Isabelle/HOL
J Hölzl
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017
122017
Noninterfering schedulers
A Popescu, J Hölzl, T Nipkow
International Conference on Algebra and Coalgebra in Computer Science, 236-252, 2013
122013
The system can't perform the operation now. Try again later.
Articles 1–20