Lawrence Paulson
Lawrence Charles Paulson is an American computer scientist. He is a Professor of Computational Logic at the University of [Cambridge Computer Laboratory] and a Fellow of Clare College, Cambridge.
Education
Paulson graduated from the California Institute of Technology in 1977, and obtained his PhD in Computer Science from Stanford University in 1981 for research on programming languages and compiler-compilers supervised by John L. Hennessy.Research
Paulson came to the University of Cambridge in 1983 and became a Fellow of Clare College, Cambridge in 1987. He is best known for the cornerstone text on the programming language ML, ML for the Working Programmer. His research is based around the interactive theorem prover Isabelle, which he introduced in 1986. He has worked on the verification of cryptographic protocols using inductive definitions, and he has also formalised the constructible universe of Kurt Gödel. Recently he has built a new theorem prover, MetiTarski, for real-valued special functions.Paulson taught an undergraduate lecture course in the Computer Science Tripos, entitled Logic and Proof which covers automated theorem proving and related methods. He also used to teach Foundations of Computer Science which introduces functional programming, but this course was taken over by Alan Mycroft and Amanda Prorok in 2017, and then Anil Madhavapeddy and Amanda Prorok in 2019.