Professor of Computational Logic
My research concerns automated theorem proving (what's that?) and its applications:
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 work on LCF 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 work 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 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: 8 February, 2012