DBLP list of my publications

My copies of the pdfs (The original publication is copyright, and available at www.springerlink.com, or from the ACM.)

• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• CakeML: A Verified Implementation of ML
• Challenges in using OpenTheory to Transport Harrison's Model from HOL Light to HOL4 (also see EPiC)
• Steps Towards Verified Implementations of HOL Light
• Standalone Tactics using OpenTheory
• Validating QBF Invalidity in HOL4 (also see Tjark Weber's copy)
• Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study
• (Nominal) Unification by Recursive Descent with Triangular Substitutions
• Bottom-Avoiding Streams