Larry Paulson's photo

15 JJ Thomson Avenue
University of Cambridge

CB3 0FD, England

Phone: (01223) 334623
Mail: lp15@cam.ac.uk
PGP key

Susan Paulson 1959–2010

Director of Research
Computer LaboratoryUniversity of Cambridge

ORCID iD iconorcid.org/0000-0003-0288-4279

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.

Research

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 logoIsabelle 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.

Academic Career

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.

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.

Researcher, Don’t Make Your Readers Scream!

Various historical downloads are available.

Last revised: Tuesday, 15 November 2022