| Publication | Date of Publication | Type |
|---|
| A Verified Compositional Algorithm for AI Planning | 2023-02-03 | Paper |
| Mechanised modal model theory | 2022-11-09 | Paper |
| Mechanisation of the AKS algorithm | 2021-06-09 | Paper |
| TacticToe: learning to prove with tactics | 2021-06-09 | Paper |
| Proof-producing synthesis of CakeML from monadic HOL functions | 2020-11-02 | Paper |
| The verified CakeML compiler backend | 2019-11-22 | Paper |
| A String of Pearls: Proofs of Fermat's Little Theorem | 2019-09-18 | Paper |
| Classification of finite fields with applications | 2019-09-02 | Paper |
| Proof pearl: Bounding least common multiples with triangles | 2019-02-18 | Paper |
| Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions | 2018-10-18 | Paper |
| Verifying the LTL to Büchi automata translation via very weak alternating automata | 2018-10-04 | Paper |
| Formally verified algorithms for upper-bounding state space diameters | 2018-08-21 | Paper |
| Verified Characteristic Formulae for CakeML | 2017-05-19 | Paper |
| Proof Pearl: Bounding Least Common Multiples with Triangles | 2016-10-27 | Paper |
| Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems | 2015-09-14 | Paper |
| Mechanisation of AKS Algorithm: Part 1 – The Main Theorem | 2015-09-14 | Paper |
| Types, bytes, and separation logic | 2014-09-12 | Paper |
| CakeML | 2014-04-10 | Paper |
| A mechanisation of some context-free language theory in HOL4 | 2013-12-13 | Paper |
| Tableaux for Verification of Data-Centric Processes | 2013-10-04 | Paper |
| Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1 | 2013-08-07 | Paper |
| Formalizing adequacy: a case study for higher-order abstract syntax | 2013-08-01 | Paper |
| A String of Pearls: Proofs of Fermat’s Little Theorem | 2013-04-19 | Paper |
| Mechanised Computability Theory | 2011-08-17 | Paper |
| Mechanisation of PDA and Grammar Equivalence for Context-Free Languages | 2010-09-29 | Paper |
| (Nominal) Unification by Recursive Descent with Triangular Substitutions | 2010-09-14 | Paper |
| A Formalisation of the Normal Forms of Context-Free Grammars in HOL4 | 2010-09-03 | Paper |
| Complete Integer Decision Procedures as Derived Rules in HOL | 2010-05-07 | Paper |
| Rewriting conversions implemented with continuations | 2010-01-25 | Paper |
| Verified, Executable Parsing | 2009-03-31 | Paper |
| Barendregt’s Variable Convention in Rule Inductions | 2009-03-06 | Paper |
| A Brief Overview of HOL4 | 2008-12-04 | Paper |
| Proof Pearl: De Bruijn Terms Really Do Work | 2008-09-02 | Paper |
| Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations | 2006-11-17 | Paper |
| Theorem Proving in Higher Order Logics | 2006-07-06 | Paper |
| Theorem Proving in Higher Order Logics | 2005-08-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4738362 | 2004-08-11 | Paper |
| A Thread of HOL Development | 2002-04-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2729073 | 2001-11-06 | Paper |
