| Verified Compilation and Optimization of Floating-Point Programs in CakeML | 0 | 0.34 | 2022 |
| Candle: A Verified Implementation of HOL Light | 0 | 0.34 | 2022 |
| Tactictoe: Learning To Prove With Tactics | 1 | 0.35 | 2021 |
| Proof-Producing Synthesis of CakeML from Monadic HOL Functions | 0 | 0.34 | 2020 |
| Verified compilation on a verified processor | 0 | 0.34 | 2019 |
| The verified CakeML compiler backend. | 2 | 0.38 | 2019 |
| Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. | 1 | 0.37 | 2018 |
| Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). | 0 | 0.34 | 2018 |
| Learning to Prove with Tactics. | 1 | 0.35 | 2018 |
| Clocked Definitions in HOL. | 0 | 0.34 | 2018 |
| Verified Characteristic Formulae for CakeML. | 0 | 0.34 | 2017 |
| Verified compilation of CakeML to multiple machine-code targets. | 3 | 0.39 | 2017 |
| Verifying efficient function calls in CakeML | 0 | 0.34 | 2017 |
| A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. | 2 | 0.37 | 2017 |
| Verified Characteristic Formulae for CakeML. | 3 | 0.39 | 2017 |
| A Proof Strategy Language and Proof Script Generation for Isabelle. | 3 | 0.62 | 2016 |
| Functional Big-Step Semantics. | 13 | 0.71 | 2016 |
| Self-Formalisation of Higher-Order Logic | 1 | 0.35 | 2016 |
| A verified type system for CakeML. | 2 | 0.40 | 2015 |
| Proof-Producing Reflection for HOL - With an Application to Model Polymorphism. | 0 | 0.34 | 2015 |
| HOL with Definitions: Semantics, Soundness, and a Verified Implementation. | 11 | 0.75 | 2014 |
| CakeML: a verified implementation of ML | 83 | 2.49 | 2014 |
| Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4. | 0 | 0.34 | 2013 |
| Steps towards verified implementations of HOL light | 8 | 0.62 | 2013 |
| Standalone Tactics Using OpenTheory. | 1 | 0.35 | 2012 |
| Validating QBF validity in HOL4 | 0 | 0.34 | 2011 |
| Formal verification of real-time data processing of the LHC beam loss monitoring system: a case study | 0 | 0.34 | 2011 |
| (Nominal) unification by recursive descent with triangular substitutions | 6 | 0.60 | 2010 |
