24 Aug. 2015    ITP 2015
Pattern Matches in HOL: A New Representation and Improved Code Generation (slides)
13 Aug. 2012    ITP 2012
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm (slides)
29 Feb. 2012    Club2
A Formalisation of Finite Automata in Isabelle/HOL (slides, printer version)
1 Feb. 2011    ARG Lunch
Quantifier Heurististics in HOL4 (slides, printer version)
18 Aug. 2010    VSTTE'10 - Theory Workshop
Local Reasoning about While-Loops (slides, paper)
26 Jan. 2010    ARG Lunch
A demo of Holfoot (slides, printer version)
24 Nov. 2009    ARG Lunch
A presentation of some tools used for Holfoot (slides, printer version)
19 Aug. 2009    TPHOLs
A formalisation of Smallfoot in HOL (slides, printer version)
5 May 2009    ARG Lunch
A Heap of Problems (slides, printer version)
27 Jan. 2009    ARG Lunch
A HOL implementation of Smallfoot (slides, printer version)
2 Sep. 2008    Research & review meeting
A fully-expansive HOL implementation of Smallfoot (slides, printer version)
19 Feb. 2008    ARG Lunch
An Embedding of Abstract Separation Logic in HOL (slides, printer version)
26 Jun. 2007    ARG Lunch
A Deep Embedding of a Decidable Fragment of Separation Logic in HOL (slides, detailed documentation)
7 Nov. 2006    ARG Lunch
A verifying ARM compiler (slides, printer version)
23 Oct. 2006    Haifa Verification Conference
Model Checking PSL using HOL and SMV (slides, printer version)
21 Jun. 2006    ARG Lunch
Deep Embeddings of Temporal Logics in HOL (slides, printer version)
1 Feb. 2006    ARG Lunch
PSL in HolCheck (slides, printer version)
23 Aug. 2005    TPHOLs
From PSL to LTL: A Formal Validation in HOL (slides, printer version)