*Director of Research*

**Computer Laboratory • University of Cambridge**

ERC project ALEXANDRIA: *making proof assistants useful to mathematicians*

My blog, Machine Logic

I am semi-retired, so I unfortunately **cannot take on new PhD students**.

My research concerns automated theorem proving and its applications:

- development of Isabelle, with emphasis on automation
- formalising mathematics, including Gödel's
*incompeteness theorems*and constructible universe

- MetiTarski, an automatic prover for the elementary functions

- proving the correctness of security protocols

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.

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. In 2013, I completed the first machine-assisted formalisation of Gödel's second incompleteness theorem.

My best-known research concerns verifying cryptographic protocols using an inductive model. But somehow the most popular of my many publications are my 1997 lecture notes on software engineering!

I was elected an ACM Fellow in 2008 for contributions to theorem provers and verification techniques.

The Royal Society elected me to a Fellowship in 2017. In that year I also received the Herbrand Award for Distinguished Contributions to Automated Reasoning.

I arrived at Cambridge in 1982 (though in fact my employer was the University of Edinburgh). In 1984, I was appointed to a permanent academic position at Cambridge as an Assistant Director of Research. Thirty-eight years later I am no longer lecturing, but material from some of my past courses is online.

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 historical downloads are available.

Last revised: Wednesday, 15 February 2023