Lawrence Paulson

From Wikipedia, the free encyclopedia
Jump to: navigation, search
Lawrence Paulson
Born Lawrence Charles Paulson
1955 (age 61–62)
Citizenship US/UK
Institutions University of Cambridge
Alma mater
Thesis A Compiler Generator for Semantic Grammars (1981)
Doctoral advisor John L. Hennessy[2]
Doctoral students
Known for
Notable awards
  • Susan Mary Paulson (d. 2010)
  • Elena Tchougounova

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.[1][2][8][9][10][11][6]


Paulson graduated from the California Institute of Technology in 1977,[12] and obtained his PhD in Computer Science from Stanford University in 1981 for research supervised by John L. Hennessy.[2][13]


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.[14][15] His research is based around the interactive theorem prover Isabelle, which he introduced in 1986.[16] He has worked on the verification of cryptographic protocols using inductive definitions,[17] and he has also formalized the constructible universe of Kurt Gödel. Recently he has built a new theorem prover, MetiTarski,[7] for real-valued special functions.[18]

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

Awards and honours[edit]

Paulson was elected a Fellow of the Royal Society (FRS) in 2017,[6] a Fellow of the Association for Computing Machinery (2008)[21] and a Distinguished Affiliated Professor for Logic in Informatics at TU Munich.[22]

Personal life[edit]

Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010.[23] He is now[when?] married to Dr Elena Tchougounova.


  1. ^ a b Lawrence Paulson publications indexed by Google Scholar
  2. ^ a b c d e f Lawrence Paulson at the Mathematics Genealogy Project
  3. ^ Fleuriot, Jacques Désiré (1990). A combination of geometry theorem proving and nonstandard analysis, with application to Newton's Principia. (PhD thesis). University of Cambridge. OCLC 964354126. 
  4. ^ Kammüller, Florian (1999). Modular reasoning in Isabelle. (PhD thesis). University of Cambridge. OCLC 43649212. 
  5. ^ Wolfram, David (1990). The Clausal Theory of Types. (PhD thesis). University of Cambridge. OCLC 59897938. 
  6. ^ a b c Anon (2017). "Professor Lawrence Paulson FRS". London: Royal Society. Retrieved 2017-05-05. 
  7. ^ a b Akbarpour, B.; Paulson, L. C. (2009). "Meti Tarski: An Automatic Theorem Prover for Real-Valued Special Functions". Journal of Automated Reasoning. 44 (3): 175. doi:10.1007/s10817-009-9149-2. 
  8. ^ List of publications from Microsoft Academic Search[dead link]
  9. ^ Lawrence Paulson author profile page at the ACM Digital Library
  10. ^ Lawrence C. Paulson at DBLP Bibliography Server
  11. ^ Lawrence Paulson's publications indexed by the Scopus bibliographic database, a service provided by Elsevier. (subscription required)
  12. ^ Paulson Entry at ORCID
  13. ^ Paulson, Lawrence Charles (1981). A Compiler Generator for Semantic Grammars. (PhD thesis). Stanford University. OCLC 757240716. 
  14. ^ Paulson, Lawrence (1996). ML for the working programmer. Cambridge New York: Cambridge University Press. ISBN 052156543X. 
  15. ^ "ML for the Working Programmer". University of Cambridge. Retrieved 25 November 2015. 
  16. ^ Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming. 3 (3): 237. doi:10.1016/0743-1066(86)90015-4. 
  17. ^ Paulson, Lawrence C. (1998). "The inductive approach to verifying cryptographic protocols". Journal of Computer Security. 6 (1-2): 85–128. ISSN 1875-8924. doi:10.3233/JCS-1998-61-205. 
  18. ^ Paulson, L. C. (2012). "Meti Tarski: Past and Future". Interactive Theorem Proving. Lecture Notes in Computer Science. 7406. p. 1. ISBN 978-3-642-32346-1. doi:10.1007/978-3-642-32347-8_1. 
  19. ^ Paulson, Larry. "Foundations of Computer Science". Retrieved 25 November 2015. 
  20. ^ Paulson, Larry. "Logic and Proof". University of Cambridge. Retrieved 25 November 2015. 
  21. ^ Anon (2008). "Professor Lawrence C. Paulson". Association for Computing Machinery. Retrieved 12 April 2016. 
  22. ^ "Certificate of Appointment" (PDF). TU Munich. Retrieved 12 April 2016. 
  23. ^ Paulson, Laurence (2010). "Susan Paulson, PhD (1959–2010)". Retrieved 25 November 2015.