*Professor of Computational Logic*

**Computer Laboratory • University of Cambridge**

ML for the Working Programmer: full text now online!

My research concerns automated theorem proving and its applications:

- development of Isabelle, with emphasis on automation
- MetiTarski, an automatic prover for the elementary functions

- formalising mathematics, including Gödel's
*incompeteness theorems*and constructible universe

- 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. I have recently 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 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 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.

Usage statistics and various downloads are available.

Last revised: 12 September, 2017