Lawrence Paulson  

Born  Lawrence Charles Paulson 1955 (age 65–66)^{[1]} 
Citizenship  US/UK 
Alma mater  
Known for  
Spouse(s) 

Awards 

Scientific career  
Fields 

Institutions  University of Cambridge Technical University of Munich 
Thesis  A Compiler Generator for Semantic Grammars (1981) 
Doctoral advisor  John L. Hennessy^{[6]} 
Website  www 
Lawrence Charles Paulson FRS^{[2]} (born 1955)^{[1]} 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.^{[5]}^{[6]}^{[7]}^{[8]}^{[9]}
Paulson graduated from the California Institute of Technology in 1977,^{[10]} and obtained his PhD in Computer Science from Stanford University in 1981 for research on programming languages and compilercompilers supervised by John L. Hennessy.^{[6]}^{[11]}
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.^{[12]}^{[13]} His research is based around the interactive theorem prover Isabelle, which he introduced in 1986.^{[14]} He has worked on the verification of cryptographic protocols using inductive definitions,^{[15]} and he has also formalised the constructible universe of Kurt Gödel. Recently he has built a new theorem prover, MetiTarski,^{[3]} for realvalued special functions.^{[16]}
Paulson teaches an undergraduate lecture course in the Computer Science Tripos, entitled Logic and Proof^{[17]} which covers automated theorem proving and related methods. (He used to teach Foundations of Computer Science^{[18]} which introduces functional programming, but this course was taken over by Alan Mycroft and Amanda Prorok in 2017,^{[19]} and then Anil Madhavapeddy and Amanda Prorok in 2019.^{[20]} )
Paulson was elected a Fellow of the Royal Society (FRS) in 2017,^{[2]} a Fellow of the Association for Computing Machinery in 2008^{[4]} and a Distinguished Affiliated Professor for Logic in Informatics at the Technical University of Munich.^{[when?]}^{[21]}
Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010.^{[22]} Since 2012, he has been married to Dr Elena Tchougounova.^{[1]}