Isabelle Workshop 2014
will be part of the
Vienna Summer of Logic

Larry Paulson's photo

15 JJ Thomson Avenue
University of Cambridge

CB3 0FD, England

Tel: (01223) 334623

Susan Paulson 1959–2010

Professor of Computational Logic
Computer Laboratory
of Cambridge

My research concerns automated theorem proving and its applications:Isabelle logo

TUM logoIsabelle, the widely-used generic theorem prover, was 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.

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 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. I have recently completed the first machine-assisted formalisation of Gödel's second incompleteness theorem. This extends the first incompleteness theorem to state that any suitable formal system that can prove its own consistency is in fact inconsistent.

My best-known research 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 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.

Clare CollegeI 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.

Locations of visitors to this page

Last revised: 9 April, 2014