| Publication | Date of Publication | Type |
|---|
| A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks | 2023-06-20 | Paper |
A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
Journal of Automated Reasoning | 2022-12-12 | Paper |
Quotients of Bounded Natural Functors
Automated Reasoning | 2022-11-09 | Paper |
scientific article; zbMATH DE number 7471712 (Why is no real title available?)
(available as arXiv preprint) | 2022-02-09 | Paper |
| scientific article; zbMATH DE number 7471712 (Why is no real title available?) | 2022-02-09 | Paper |
CryptHOL: game-based proofs in higher-order logic
Journal of Cryptology | 2020-04-28 | Paper |
Effect polymorphism in higher-order logic (proof pearl)
Journal of Automated Reasoning | 2019-08-21 | Paper |
Automatic refinement to efficient data structures: a comparison of two approaches
Journal of Automated Reasoning | 2019-05-31 | Paper |
| Fast machine words in Isabelle/HOL | 2018-10-04 | Paper |
| Relational parametricity and quotient preservation for modular (co)datatypes | 2018-10-04 | Paper |
Mechanising a type-safe model of multithreaded Java with a verified compiler
Journal of Automated Reasoning | 2018-08-21 | Paper |
| Foundational (co)datatypes and (co)recursion for higher-order logic | 2018-01-04 | Paper |
Effect polymorphism in higher-order logic (proof pearl)
Interactive Theorem Proving | 2018-01-04 | Paper |
Friends with benefits. Implementing corecursion in foundational proof assistants
Programming Languages and Systems | 2017-05-19 | Paper |
Equational Reasoning with Applicative Functors
Interactive Theorem Proving | 2016-10-27 | Paper |
Probabilistic functions and cryptographic oracles in higher order logic
Programming Languages and Systems | 2016-04-26 | Paper |
A formalized hierarchy of probabilistic system types. Proof pearl
Interactive Theorem Proving | 2015-09-14 | Paper |
Stream Fusion for Isabelle’s Code Generator
Interactive Theorem Proving | 2015-09-14 | Paper |
Truly modular (co)datatypes for Isabelle/HOL
Interactive Theorem Proving | 2014-09-08 | Paper |
Recursive Functions on Lazy Lists via Domains and Topologies
Interactive Theorem Proving | 2014-09-08 | Paper |
Light-weight containers for Isabelle: efficient, extensible, nestable
Interactive Theorem Proving | 2013-08-07 | Paper |
Java and the Java memory model -- a unified, machine-checked formalisation
Programming Languages and Systems | 2012-06-22 | Paper |
Animating the formalised semantics of a Java-like language
Interactive Theorem Proving | 2011-08-17 | Paper |
The Isabelle collections framework
Interactive Theorem Proving | 2010-09-14 | Paper |
Verifying a Compiler for Java Threads
Programming Languages and Systems | 2010-05-04 | Paper |
Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
Lecture Notes in Computer Science | 2009-10-20 | Paper |
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
Lecture Notes in Computer Science | 2008-12-04 | Paper |
The computational complexity of evolutionarily stable strategies
International Journal of Game Theory | 2008-05-26 | Paper |
