Lawrence C. Paulson

Professor of Computational Logic

Computer Laboratory, University of Cambridge, UK

	Publications and Grants
	Isabelle theorem prover Projects done using Isabelle
	Curriculum Vitae
	The book ML for the Working Programmer

My research concerns mechanical theorem proving and its applications:

• continued development of the interactive theorem prover Isabelle
• applying automated theorem provers to verification problems
• applying set theory to specification and verification
• mechanizing selected areas of mathematics

The Isabelle system is a popular generic theorem prover, developed in collaboration with Tobias Nipkow and his colleagues at T. U. Munich. 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 formlized 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. Recent research grants concern a variety of projects involving fully automatic proof.

Material related to my recently finished Isabelle lecture course.

I am a Fellow of Clare College.

I am also the Distinguished Affiliated Professor for Logic in Informatics at T. U. Munich.

Usage statistics for my pages are available, and various downloads. I have also built another site.

Telephone: (01223) 334623
Fax:       (01223) 334678
E-mail: lcp@cl.cam.ac.uk

PGP : D8 A7 F0 F4 0B FE 38 DB 2B CF 7C 8C 6A 1A 3E 04