Lawrence Paulson Explained

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,^[1] 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.^[2]

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.^{[3] [4]} His research is based around the interactive theorem prover Isabelle, which he introduced in 1986.^[5] He has worked on the verification of cryptographic protocols using inductive definitions,^[6] 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.^[7]

Paulson teaches an undergraduate lecture course in the Computer Science Tripos, entitled Logic and Proof^[8] which covers automated theorem proving and related methods. (He used to teach Foundations of Computer Science^[9] which introduces functional programming, but this course was taken over by Alan Mycroft and Amanda Prorok in 2017,^[10] and then Anil Madhavapeddy and Amanda Prorok in 2019.^[11])

Awards and honours

Paulson was elected a Fellow of the Royal Society (FRS) in 2017, a Fellow of the Association for Computing Machinery in 2008^[12] and a Distinguished Affiliated Professor for Logic in Informatics at the Technical University of Munich.^[13]

Personal life

Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010.^[14] Since 2012, he has been married to Dr Elena Tchougounova.

Notes and References

1. Lawrence Paulson
2. PhD . Lawrence Charles. Paulson . A Compiler Generator for Semantic Grammars . cl.cam.ac.uk. 1981 . Lawrence Paulson. 757240716. Stanford University.
3. Book: Paulson, Lawrence . ML for the working programmer . Cambridge University Press . Cambridge New York . 1996 . 978-0521565431 .
4. Web site: ML for the Working Programmer. University of Cambridge. 25 November 2015.
5. 10.1016/0743-1066(86)90015-4. Natural deduction as higher-order resolution. The Journal of Logic Programming. 3. 3. 237–258. 1986. Paulson . L. C. . cs/9301104. 27085090.
6. Paulson. Lawrence C.. The inductive approach to verifying cryptographic protocols. Journal of Computer Security. 6. 1–2. 1998. 85–128. 1875-8924. 10.3233/JCS-1998-61-205 . 2105.06319. 10.1.1.57.2049. 7591720 .
7. Book: 10.1007/978-3-642-32347-8_1. Meti Tarski: Past and Future. Interactive Theorem Proving. 7406. 1–10. Lecture Notes in Computer Science. 2012. Paulson . L. C. . 978-3-642-32346-1. 10.1.1.259.5577.
8. Web site: Logic and Proof. Paulson. Larry. University of Cambridge. 27 January 2020.
9. Web site: Foundations of Computer Science. Paulson. Larry. 25 November 2015.
10. Web site: Department of Computer Science and Technology – Course pages 2017–18: Foundations of Computer Science. www.cl.cam.ac.uk. 2020-01-27.
11. Web site: Department of Computer Science and Technology – Course pages 2019–20: Foundations of Computer Science. www.cl.cam.ac.uk. 2020-01-27.
12. Web site: Professor Lawrence C. Paulson. awards.acm.org. Anon. 2008. Association for Computing Machinery. 12 April 2016.
13. Web site: Certificate of Appointment. TU Munich. 12 April 2016.
14. Web site: Susan Paulson, PhD (1959–2010). 25 November 2015. Lawrence. Paulson. 2010. University of Cambridge.