Lawrence Paulson

Lawrence Charles Paulson (born 1955) is a professor at the University of Cambridge Computer Laboratory and a fellow of Clare College. He teaches two undergraduate lecture courses, entitled Foundations of Computer Science (which introduces functional programming) and Logic and Proof (which covers automated theorem proving and related methods). 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 formalized the constructible universe of Kurt Gödel. Recently he has built a new theorem prover, MetiTarski, for real-valued special functions. Current research projects are described on his web page.

Paulson graduated from the California Institute of Technology in 1977, and obtained his PhD in Computer Science from Stanford University. He came to the University of Cambridge in 1983 and became a Fellow of Clare College in 1987. He has two children by his first wife, Dr Susan Mary Paulson, who died 2010. He is now married to Dr Elena Tchougounova. He is a Fellow of the Association for Computing Machinery (2008).

External links

• Lawrence Paulson's website