13 April 2018 ARW 2018 Real-world formal documentation (slides, abstract)
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)