Some of my presentations
Here are PDF slides for some of the reserach talks that I have given.
A new verified compiler backend for CakeMLA guest lecture on compiler verification
Turning proof assistants into programming assistants
Functional big-step semantics
Towards verified theorem provers
CakeML: a verified implementation of ML
Machine-code verification: Experience of tackling medium-sized case studies using decompilation into logic
Translation validation for a verified OS kernel
Machine code, formal verification and functional programming
Steps towards verified implementations of HOL Light
Decompilation into Logic — Improved
A verified runtime for a verified theorem prover
Separation logic adapted for proofs by rewriting
Extensible proof-producing compilation
Mechanically verified Lisp intepreters
Proof-producing decompilation and compilation
Hoare logic for realistically modelled machine code