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!
  
• 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.

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: 4 April, 2013