| Truly modular (co) datatypes for Isabelle/HOL JC Blanchette, J Hölzl, A Lochbihler, L Panny, A Popescu, D Traytel Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as …, 2014 | 126 | 2014 |
| Type classes and filters for mathematical analysis in Isabelle/HOL J Hölzl, F Immler, B Huffman Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013 | 121 | 2013 |
| Three chapters of measure theory in Isabelle/HOL J Hölzl, A Heller International Conference on Interactive Theorem Proving, 135-151, 2011 | 113 | 2011 |
| Numerical analysis of ordinary differential equations in Isabelle/HOL F Immler, J Hölzl Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012 | 69 | 2012 |
| 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 | 59 | 2017 |
| Proving inequalities over reals with computation in Isabelle/HOL J Hölzl Proceedings of the ACM SIGSAM 2009 International Workshop on Programming …, 2009 | 42 | 2009 |
| Construction and stochastic applications of measure spaces in higher-order logic J Hölzl Technische Universität München, 2013 | 37 | 2013 |
| Markov chains and Markov decision processes in Isabelle/HOL J Hölzl Journal of Automated Reasoning 59 (3), 345-387, 2017 | 35 | 2017 |
| 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 | 34 | 2010 |
| A verified compiler for probability density functions M Eberl, J Hölzl, T Nipkow Programming Languages and Systems: 24th European Symposium on Programming …, 2015 | 33 | 2015 |
| Formalizing the solution to the cap set problem SR Dahmen, J Hölzl, RY Lewis arXiv preprint arXiv:1907.01449, 2019 | 24 | 2019 |
| Proving concurrent noninterference A Popescu, J Hölzl, T Nipkow Certified Programs and Proofs: Second International Conference, CPP 2012 …, 2012 | 24 | 2012 |
| Formalising semantics for expected running time of probabilistic programs J Hölzl Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy …, 2016 | 21 | 2016 |
| Foundational (co) datatypes and (co) recursion for higher-order logic J Biendarra, JC Blanchette, A Bouzy, M Desharnais, M Fleury, J Hölzl, ... Frontiers of Combining Systems: 11th International Symposium, FroCoS 2017 …, 2017 | 20 | 2017 |
| A Formalized Hierarchy of Probabilistic System Types: Proof Pearl J Hölzl, A Lochbihler, D Traytel Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing …, 2015 | 19 | 2015 |
| Markov processes in Isabelle/HOL J Hölzl Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 17 | 2017 |
| Recursive functions on lazy lists via domains and topologies A Lochbihler, J Hölzl International Conference on Interactive Theorem Proving, 341-357, 2014 | 17 | 2014 |
| Formalizing probabilistic noninterference A Popescu, J Hölzl, T Nipkow Certified Programs and Proofs: Third International Conference, CPP 2013 …, 2013 | 17 | 2013 |
| Verifying pCTL model checking J Hölzl, T Nipkow International Conference on Tools and Algorithms for the Construction and …, 2012 | 16 | 2012 |
| Noninterfering Schedulers: When Possibilistic Noninterference Implies Probabilistic Noninterference A Popescu, J Hölzl, T Nipkow International Conference on Algebra and Coalgebra in Computer Science, 236-252, 2013 | 12 | 2013 |
Andrei PopescuUniversity of SheffieldVerified email at sheffield.ac.uk
