## 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