My research concerns automated theorem proving and its applications:
During the 1980s, my research on LCF-style theorem proving introduced concepts such as conversions and theorem continuations, which are still mainstays of HOL theorem prover. I helped design the programming language Standard ML and have written one of the main textbooks, ML for the Working Programmer.
Isabelle appeared in 1986, and was later developed in collaboration with Tobias Nipkow and his colleagues at the Technical University of Munich. I am now the Distinguished Affiliated Professor for Logic in Informatics at TUM, honouring my long-standing relationship with that institution. I was elected an ACM Fellow in 2008.
During the 1990s, Isabelle found a worldwide user community. I investigated the mechanization of induction and recursion and their duals, coinduction and corecursion. Early in the 2000s, I formalized deep results of set theory: the reflection theorem and the relative consistency of the axiom of choice. I have recently completed the first machine-assisted formalisation of Gödel's second incompleteness theorem.
I teach two undergraduate lecture courses: Foundations of Computer Science (an introduction to programming and algorithms, using Standard ML), and Logic and Proof (covering automatic theorem-proving technologies such as resolution and SAT-solving). My Master's-level course, Interactive Formal Verification, is a hands-on introduction to Isabelle.
I am a Fellow of Clare College, where I have responsibility for admitting and supervising Computer Science students. I sit on Clare's Governing Body and on various committees.
I have long served as an editor of the Journal of Automated Reasoning and on the Programme Committees of numerous conferences. I was a founding editor of LMS Journal of Computation and Mathematics until 2007.
Various downloads are available.
Last revised: 18 September, 2014