| Publication | Date of Publication | Type |
|---|
Candle: a verified implementation of HOL Light (extended version)
Journal of Automated Reasoning | 2026-02-06 | Paper |
Fast, verified computation for HOL ITPs
Journal of Automated Reasoning | 2025-03-20 | Paper |
| Certified MaxSAT preprocessing | 2025-01-31 | Paper |
| Fast, verified computation for candle | 2024-11-26 | Paper |
| Candle: a verified implementation of HOL light | 2024-07-15 | Paper |
| Taming an authoritative armv8 ISA specification: L3 validation and cakeml compiler verification | 2024-07-15 | Paper |
Icing: supporting fast-math style optimizations in a verified compiler
Computer Aided Verification | 2024-02-16 | Paper |
| scientific article; zbMATH DE number 7699418 (Why is no real title available?) | 2023-06-20 | Paper |
| Characteristic formulae for liveness properties of non-terminating CakeML programs | 2023-02-03 | Paper |
Automatically Introducing Tail Recursion in CakeML
Lecture Notes in Computer Science | 2022-12-09 | Paper |
| \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML | 2021-10-18 | 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 verified generational garbage collector for CakeML
Journal of Automated Reasoning | 2019-08-21 | Paper |
| Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions | 2018-10-18 | Paper |
| Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) | 2018-10-04 | Paper |
A verified generational garbage collector for CakeML
Interactive Theorem Proving | 2018-01-04 | Paper |
Verified characteristic formulae for CakeML
Programming Languages and Systems | 2017-05-19 | Paper |
The reflective Milawa theorem prover is sound (down to the machine code that runs it)
Journal of Automated Reasoning | 2016-05-26 | Paper |
Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
Journal of Automated Reasoning | 2016-05-26 | Paper |
Pattern matches in HOL: a new representation and improved code generation
Interactive Theorem Proving | 2015-09-14 | Paper |
Verified just-in-time compiler on x86
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-06-11 | Paper |
Transforming programs into recursive functions
Electronic Notes in Theoretical Computer Science | 2015-03-19 | Paper |
The reflective Milawa theorem prover is sound (down to the machine code that runs it)
Interactive Theorem Proving | 2014-09-08 | Paper |
HOL with definitions: semantics, soundness, and a verified implementation
Interactive Theorem Proving | 2014-09-08 | Paper |
Proof-producing translation of higher-order logic into pure and stateful ML
Journal of Functional Programming | 2014-08-14 | Paper |
Proof-producing synthesis of ML from higher-order logic
Proceedings of the 17th ACM SIGPLAN international conference on Functional programming | 2014-07-21 | Paper |
CakeML
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Steps towards Verified Implementations of HOL Light
Interactive Theorem Proving | 2013-08-07 | Paper |
Function extraction
Science of Computer Programming | 2012-07-20 | Paper |
A verified runtime for a verified theorem prover
Interactive Theorem Proving | 2011-08-17 | Paper |
A trustworthy monadic formalization of the ARMv7 instruction set architecture
Interactive Theorem Proving | 2010-09-14 | Paper |
Separation logic adapted for proofs by rewriting
Interactive Theorem Proving | 2010-09-14 | Paper |
Hoare Logic for ARM Machine Code
Lecture Notes in Computer Science | 2008-07-01 | Paper |
Hoare Logic for Realistically Modelled Machine Code
Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-03 | Paper |
