×
Compute Distance To:
Author ID: holzl.johannes Recent zbMATH articles by "Hölzl, Johannes"
Published as: Hölzl, Johannes; Hölzl, J.
Documents Indexed: 19 Publications since 1992
Co-Authors: 26 Co-Authors with 17 Joint Publications
402 Co-Co-Authors

Publications by Year

Citations contained in zbMATH Open

15 Publications have been cited 103 times in 70 Documents Cited by Year
Type classes and filters for mathematical analysis in Isabelle/HOL. Zbl 1317.68213
Hölzl, Johannes; Immler, Fabian; Huffman, Brian
22
2013
Three chapters of measure theory in Isabelle/HOL. Zbl 1342.68287
Hölzl, Johannes; Heller, Armin
21
2011
Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151
Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy
18
2014
Numerical analysis of ordinary differential equations in Isabelle/HOL. Zbl 1360.68753
Immler, Fabian; Hölzl, Johannes
10
2012
A formalized hierarchy of probabilistic system types. Proof pearl. Zbl 1465.68199
Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy
6
2015
Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 06821624
Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy
5
2017
A formally verified proof of the central limit theorem. Zbl 1425.68369
Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke
5
2017
A verified compiler for probability density functions. Zbl 1335.68037
Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias
4
2015
Markov chains and Markov decision processes in Isabelle/HOL. Zbl 1425.68375
Hölzl, Johannes
3
2017
Formalising semantics for expected running time of probabilistic programs. Zbl 1478.68138
Hölzl, Johannes
2
2016
Formalizing probabilistic noninterference. Zbl 1426.68287
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
2
2013
Recursive functions on lazy lists via domains and topologies. Zbl 1416.68169
Lochbihler, Andreas; Hölzl, Johannes
2
2014
Verifying pCTL model checking. Zbl 1352.68154
Hölzl, Johannes; Nipkow, Tobias
1
2012
Proving concurrent noninterference. Zbl 1383.68014
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
1
2012
Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference. Zbl 1394.68083
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
1
2013
Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 06821624
Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy
5
2017
A formally verified proof of the central limit theorem. Zbl 1425.68369
Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke
5
2017
Markov chains and Markov decision processes in Isabelle/HOL. Zbl 1425.68375
Hölzl, Johannes
3
2017
Formalising semantics for expected running time of probabilistic programs. Zbl 1478.68138
Hölzl, Johannes
2
2016
A formalized hierarchy of probabilistic system types. Proof pearl. Zbl 1465.68199
Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy
6
2015
A verified compiler for probability density functions. Zbl 1335.68037
Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias
4
2015
Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151
Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy
18
2014
Recursive functions on lazy lists via domains and topologies. Zbl 1416.68169
Lochbihler, Andreas; Hölzl, Johannes
2
2014
Type classes and filters for mathematical analysis in Isabelle/HOL. Zbl 1317.68213
Hölzl, Johannes; Immler, Fabian; Huffman, Brian
22
2013
Formalizing probabilistic noninterference. Zbl 1426.68287
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
2
2013
Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference. Zbl 1394.68083
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
1
2013
Numerical analysis of ordinary differential equations in Isabelle/HOL. Zbl 1360.68753
Immler, Fabian; Hölzl, Johannes
10
2012
Verifying pCTL model checking. Zbl 1352.68154
Hölzl, Johannes; Nipkow, Tobias
1
2012
Proving concurrent noninterference. Zbl 1383.68014
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
1
2012
Three chapters of measure theory in Isabelle/HOL. Zbl 1342.68287
Hölzl, Johannes; Heller, Armin
21
2011
all top 5

Cited by 109 Authors

9 Hasan, Osman
7 Blanchette, Jasmin Christian
7 Tahar, Sofiène
6 Lochbihler, Andreas
6 Paulson, Lawrence Charles
6 Popescu, Andrei
4 Traytel, Dmitry
3 Ahmed, Waqar
3 Boldo, Sylvie
3 Divasón, Jose
3 Immler, Fabian
3 Kunčar, Ondřej
3 Nipkow, Tobias
2 Abdulaziz, Mohammad
2 Affeldt, Reynald
2 Aransay, Jesús
2 Avigad, Jeremy
2 Chlipala, Adam J.
2 Coghetto, Roland
2 Elleuch, Maissa
2 Grégoire, Thomas
2 Hölzl, Johannes
2 Lammich, Peter
2 Lelay, Catherine
2 Li, Wenda
2 Matichuk, Daniel
2 Melquiond, Guillaume
2 Schlichtkrull, Anders
2 Siddique, Umair
2 Théry, Laurent
2 Traut, Christoph
2 Wenzel, Makarius
1 Abid, Mohamed Amine
1 Ahmad, Waqar
1 Aravantinos, Vincent
1 Basin, David A.
1 Bauereiß, Thomas
1 Bertot, Yves
1 Bouzy, Aymeric
1 Brunner, Julian
1 Clément, François
1 Cohen, Cyril
1 Cohen, Liron
1 Eberl, Manuel
1 Echenim, Mnacho
1 Endou, Noboru
1 Faissole, Florian
1 Fallah, Mehran S.
1 Fleury, Mathias
1 Gheri, Lorenzo
1 Gidey, Habtom Kashay
1 Greenaway, David
1 Guiol, Hervé
1 Hagiwara, Manabu
1 Hamdi, Mohammad Salah
1 Hanaoka, Goichiro
1 Haslbeck, Max W.
1 Haslbeck, Maximilian P. L.
1 Huerta y Munive, Jonathan Julián
1 Hupel, Lars
1 Iranmanesh, Zeinab
1 Johann, Patricia
1 Joosten, Sebastiaan J. C.
1 Kaliszyk, Cezary
1 Khan Afshar, Sanaz
1 Kitagawa, Fuyuki
1 Kühlwein, Daniel
1 Kuncak, Viktor
1 Lewis, Robert Y.
1 Li, Liming
1 Liu, Liya
1 Maggesi, Marco
1 Mahmoud, Mohamed Yousri
1 Marmsoler, Diego
1 Martin, Vincent
1 Matsuda, Takahiro
1 Mayero, Micaela
1 Momigliano, Alberto
1 Murray, Toby
1 Peltier, Nicolas
1 Pesenti Gritti, Armando
1 Pientka, Brigitte
1 Platzer, André
1 Polonsky, Andrew
1 Pous, Damien
1 Qasim, Muhammad
1 Raimondi, Franco
1 Reynolds, Andrew
1 Rideau, Laurence
1 Rouhling, Damien
1 Roux, Cody
1 Sangiorgi, Davide
1 Schneider, Joshua P.
1 Seddiki, Ons
1 Sefidgar, S. Reza
1 Sénizergues, Jonas
1 Serafin, Luke
1 Steinberg, Florian
1 Struth, Georg
1 Tan, Yong Kiam
...and 9 more Authors

Citations by Year