| Publication | Date of Publication | Type |
|---|
Fast, verified computation for HOL ITPs
Journal of Automated Reasoning | 2025-03-20 | Paper |
| Dependently sorted theorem proving for mathematical foundations | 2024-11-26 | Paper |
| Kalas: a verified, end-to-end compiler for a choreographic language | 2024-07-15 | Paper |
| Mechanizing soundness of off-policy evaluation | 2024-07-15 | Paper |
| A Verified Compositional Algorithm for AI Planning | 2023-02-03 | Paper |
| Mechanised modal model theory | 2022-11-09 | Paper |
Mechanisation of the AKS algorithm
Journal of Automated Reasoning | 2021-06-09 | Paper |
TacticToe: learning to prove with tactics
Journal of Automated Reasoning | 2021-06-09 | Paper |
Proof-producing synthesis of CakeML from monadic HOL functions
Journal of Automated Reasoning | 2020-11-02 | Paper |
The verified CakeML compiler backend
Journal of Functional Programming | 2019-11-22 | Paper |
| A String of Pearls: Proofs of Fermat's Little Theorem | 2019-09-18 | Paper |
Classification of finite fields with applications
Journal of Automated Reasoning | 2019-09-02 | Paper |
Proof pearl: Bounding least common multiples with triangles
Journal of Automated Reasoning | 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
Journal of Automated Reasoning | 2018-08-21 | Paper |
Verified characteristic formulae for CakeML
Programming Languages and Systems | 2017-05-19 | Paper |
Proof pearl: Bounding least common multiples with triangles
Interactive Theorem Proving | 2016-10-27 | Paper |
Verified over-approximation of the diameter of propositionally factored transition systems
Interactive Theorem Proving | 2015-09-14 | Paper |
Mechanisation of AKS algorithm. I. The main theorem
Interactive Theorem Proving | 2015-09-14 | Paper |
Types, bytes, and separation logic
Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
CakeML
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
A mechanisation of some context-free language theory in HOL4
Journal of Computer and System Sciences | 2013-12-13 | Paper |
Tableaux for verification of data-centric processes
Lecture Notes in Computer Science | 2013-10-04 | Paper |
Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
Interactive Theorem Proving | 2013-08-07 | Paper |
Formalizing adequacy: a case study for higher-order abstract syntax
Journal of Automated Reasoning | 2013-08-01 | Paper |
A string of pearls: proofs of Fermat's little theorem
Certified Programs and Proofs | 2013-04-19 | Paper |
Mechanised computability theory
Interactive Theorem Proving | 2011-08-17 | Paper |
Mechanisation of PDA and grammar equivalence for context-free languages
Logic, Language, Information and Computation | 2010-09-29 | Paper |
(Nominal) unification by recursive descent with triangular substitutions
Interactive Theorem Proving | 2010-09-14 | Paper |
A formalisation of the normal forms of context-free grammars in HOL4
Computer Science Logic | 2010-09-03 | Paper |
Complete integer decision procedures as derived rules in HOL
Lecture Notes in Computer Science | 2010-05-07 | Paper |
Rewriting conversions implemented with continuations
Journal of Automated Reasoning | 2010-01-25 | Paper |
Verified, Executable Parsing
Programming Languages and Systems | 2009-03-31 | Paper |
Barendregt’s Variable Convention in Rule Inductions
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
A Brief Overview of HOL4
Lecture Notes in Computer Science | 2008-12-04 | Paper |
Proof Pearl: De Bruijn Terms Really Do Work
Lecture Notes in Computer Science | 2008-09-02 | Paper |
Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
Higher-Order and Symbolic Computation | 2006-11-17 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2006-07-06 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2005-08-18 | Paper |
| scientific article; zbMATH DE number 2087552 (Why is no real title available?) | 2004-08-11 | Paper |
A Thread of HOL Development
The Computer Journal | 2002-04-29 | Paper |
| scientific article; zbMATH DE number 1629957 (Why is no real title available?) | 2001-11-06 | Paper |
