Professor of Computational Logic

Computer Laboratory, University of Cambridge, UK

My research concerns mechanical theorem proving and its applications:

• continued development of the interactive theorem prover Isabelle
• applying automated theorem provers to verification problems
• applying set theory to specification and verification
• mechanizing selected areas of mathematics
• MetiTarski, an automatic prover for the elementary functions

The Isabelle system is a popular generic theorem prover, 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 T. U. Munich. This honorary title reflects my long-standing relationship with that institution.

During the 1980s, my work on LCF introduced concepts such as conversions and theorem continuations, which are still mainstays of the HOL system. I was involved in the design of the programming language Standard ML and have written one of the main textbooks, ML for the Working Programmer.

During the 1990s, Isabelle found a worldwide user community. I published results on the mechanization of induction and recursion and their duals, coinduction and corecursion. I also published some work on the UNITY formalism. Early in the 2000s, I formalized deep results of set theory: the reflection theorem and the relative consistency of the axiom of choice.

My best-known work concerns verifying cryptographic protocols using an inductive model. Recent research grants concern a variety of projects involving fully automatic proof. The Cambridge Isabelle group is pursuing a variety of topics.

I am a Fellow of Clare College, where I have responsibility for admitting and supervising the progress of undergraduates reading Computer Science. I sit on Clare's Governing Body and on various committees.

I am married to Susan Paulson.

Usage statistics for my pages are available, and various downloads.

Last revised: 10 September, 2008