My research interests lie in the areas of formal methods, interactive theorem proving (I am one of the developers of the HOL4 system), and formal semantics for complicated real-world systems.
I am currently involved in the L4.verified project within NICTA (aiming to verify a modern micro-kernel), as well as work with colleagues at the University of Cambridge to produce validated formal descriptions of TCP/IP.
Bio:
I received my PhD in 1999 from the University of Cambridge, and was an undergraduate at Victoria University of Wellington.
