Professor of Computational Logic

Computer Laboratory, University of Cambridge, UK

My research concerns automated theorem proving (what's that?) and its applications:

• continued development of the interactive theorem prover Isabelle, and its integration with automated theorem provers (the popular sledgehammer tool)
• MetiTarski, an automatic prover for the elementary functions
  new project now underway!
• formalising mathematics, including Gödel's two incompeteness theorems
• verifying security protocols
• applying set theory to specification and verification, and formalising deep results including Gödel's constructible universe.

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. I was elected an ACM Fellow in 2008.

During the 1980s, my research on LCF-style theorem proving 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. I have recently completed the first machine-assisted formalisation of Gödel's second incompleteness theorem. This extends the first incompleteness theorem to state that any suitable formal system that can prove its own consistency is in fact inconsistent.

My best-known research concerns verifying cryptographic protocols using an inductive model. The Cambridge Isabelle group is pursuing a variety of topics, and Isabelle has had a global impact. But somehow the most popular by far of my many publications are my software engineering lecture notes (written in 1997)!

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 the progress of undergraduates reading Computer Science. 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.

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

Last revised: 5 June, 2013