Emeritus Professor of Computational Logic
Computer Laboratory • University of Cambridge
ERC project ALEXANDRIA: making proof assistants useful to mathematicians
My blog, Machine Logic
I am retired, so I unfortunately cannot take on new PhD students.
My research concerns automated theorem proving and its applications:Isabelle logo
ML book coverDuring 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 .
TUM logo 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.
Royal Society logo
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. Four decades later I am no longer lecturing, but material from some of my past courses is online.
Clare CollegeI 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: Thursday, 9 October 2025
