Lawrence Paulson

Lawrence Paulson
Born	Lawrence Charles Paulson 1955 (age 61–62)
Citizenship	US/UK
Fields	Theorem proving Formal methods Computer security
Institutions	University of Cambridge
Alma mater	California Institute of Technology (BSc) Stanford University (PhD)
Thesis	A Compiler Generator for Semantic Grammars (1981)
Doctoral advisor	John L. Hennessy
Doctoral students	Jacques Fleuriot Florian Kammüller David Wolfram
Known for	ML Isabelle MetiTarski
Notable awards	Pilkington Teaching Prize (2003) ACM Fellow (2008) FRS (2017)
Spouse	Susan Mary Paulson (d. 2010) Elena Tchougounova
Website www.cl.cam.ac.uk/~lp15/

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.

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.

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 formalized the constructible universe of Kurt Gödel. Recently he has built a new theorem prover, MetiTarski, for real-valued special functions.

Paulson teaches two undergraduate lecture courses on the Computer Science Tripos, entitled Foundations of Computer Science (which introduces functional programming) and Logic and Proof(which covers automated theorem proving and related methods).

...
Wikipedia