World Library  
Flag as Inappropriate
Email this Article

Lawrence Paulson

Lawrence Paulson
Born Lawrence Charles Paulson
1955 (age 60–61)
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
  • Jacques Fleuriot[3]
  • Florian Kammueller
  • David Wolfram[2][4]
Known for
Notable awards
  • Pilkington Teaching Prize (2003)
  • FACM (2008)
  • Susan Mary Paulson (d. 2010)
  • Elena Tchougounova
Lawrence Charles Paulson

(born 1955) is a professor at the University of Cambridge Computer Laboratory and a fellow of Clare College, Cambridge.[1][2][6][7][8][9]


  • Education 1
  • Research 2
  • Teaching 3
  • Personal life 4
  • Awards and honours 5
  • References 6


Paulson graduated from the California Institute of Technology in 1977, and obtained his PhD in Computer Science from Stanford University under the supervision of John L. Hennessy.[2][10]


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.[11][12] His research is based around the interactive theorem prover Isabelle, which he introduced in 1986.[13] 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,[5] for real-valued special functions.[14]


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

Personal life

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

Awards and honours

Paulson is a Fellow of the Association for Computing Machinery (2008).


  1. ^ a b Lawrence Paulson's publications indexed by Google Scholar, a service provided by Google
  2. ^ a b c d 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. 
  4. ^ Wolfram, David (1990). The Clausal Theory of Types (PhD thesis). University of Cambridge. 
  5. ^ 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.  
  6. ^ List of publications from Microsoft Academic Search
  7. ^ Lawrence Paulson from the Association for Computing Machinery (ACM) Digital Library
  8. ^ Lawrence Paulson's publications indexed by the DBLP Bibliography Server at the University of Trier
  9. ^ Lawrence Paulson's publications indexed by the Scopus bibliographic database, a service provided by Elsevier.
  10. ^ Paulson, Lawrence Charles (1981). A Compiler Generator for Semantic Grammars (PhD thesis). Stanford University. 
  11. ^ Paulson, Lawrence (1996). ML for the working programmer. Cambridge New York: Cambridge University Press.  
  12. ^
  13. ^ Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming 3 (3): 237.  
  14. ^ Paulson, L. C. (2012). "Meti Tarski: Past and Future". Interactive Theorem Proving. Lecture Notes in Computer Science 7406. p. 1.  
  15. ^
  16. ^
  17. ^

This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from World eBook Library are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.