Citizenship US/UK Role Computer scientist | Name Lawrence Paulson Known for MLIsabelleMetiTarski | |
 | ||
Thesis A Compiler Generator for Semantic Grammars (1981) Doctoral students Jacques FleuriotFlorian KammuellerDavid Wolfram Books ML for the working programmer, Logic and computation | ||
Lawrence Charles Paulson (born 1955) FRS is a professor of Computational Logic at the University of Cambridge Computer Laboratory and a Fellow of Clare College, Cambridge.
Contents
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 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 teaches only one undergraduate lecture course on the Computer Science Tripos, entitled Foundations of Computer Science (which introduces functional programming).
Awards and honours
Paulson was elected a Fellow of the Royal Society (FRS) in 2017, a Fellow of the Association for Computing Machinery (2008) and a Distinguished Affiliated Professor for Logic in Informatics at TU Munich.
Personal life
Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010. Since 2012, he has been married to Dr Elena Tchougounova.