Lawrence Paulson

Last updated

Lawrence Paulson
FRS
Lawrence Paulson Royal Society.jpg
Paulson in 2017
Born
Lawrence Charles Paulson

1955 (age 69–70) [1]
CitizenshipUS/UK
Alma mater
Known for
Spouses
  • Susan Mary Paulson (d. 2010)
  • Elena Tchougounova
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.cl.cam.ac.uk/~lp15/

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. [5] [6] [7] [8] [9]

Contents

Education

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 compiler-compilers supervised by John L. Hennessy. [6] [11]

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. [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 real-valued special functions. [16]

Paulson taught an undergraduate lecture course in the Computer Science Tripos, entitled Logic and Proof [17] which covers automated theorem proving and related methods. He also 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]

Awards and honours

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]

Personal life

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]

References

  1. 1 2 Anon (2017). "Paulson, Prof. Lawrence Charles" . Who's Who (online Oxford University Press  ed.). Oxford: A & C Black. doi:10.1093/ww/9780199540884.013.289302.(Subscription or UK public library membership required.)
  2. 1 2 Anon (2017). "Professor Lawrence Paulson FRS". royalsociety.org. London: Royal Society . Retrieved 5 May 2017.
  3. 1 2 Akbarpour, B.; Paulson, L. C. (2009). "Meti Tarski: An Automatic Theorem Prover for Real-Valued Special Functions". Journal of Automated Reasoning . 44 (3): 175. CiteSeerX   10.1.1.157.3300 . doi:10.1007/s10817-009-9149-2. S2CID   16215962.
  4. 1 2 Anon (2008). "Professor Lawrence C. Paulson". awards.acm.org. Association for Computing Machinery . Retrieved 12 April 2016.
  5. 1 2 3 4 Lawrence Paulson publications indexed by Google Scholar OOjs UI icon edit-ltr-progressive.svg
  6. 1 2 3 Lawrence Paulson at the Mathematics Genealogy Project
  7. ↑ Lawrence Paulson author profile page at the ACM Digital Library
  8. ↑ Lawrence C. Paulson at DBLP Bibliography Server OOjs UI icon edit-ltr-progressive.svg
  9. ↑ Lawrence Paulson publications indexed by the Scopus bibliographic database. (subscription required)
  10. ↑ Lawrence Paulson ORCID   0000-0003-0288-4279
  11. ↑ Paulson, Lawrence Charles (1981). A Compiler Generator for Semantic Grammars (PDF). cl.cam.ac.uk (PhD thesis). Stanford University. OCLC   757240716.
  12. ↑ Paulson, Lawrence (1996). ML for the working programmer. Cambridge New York: Cambridge University Press. ISBN   978-0521565431.
  13. ↑ "ML for the Working Programmer". University of Cambridge. Retrieved 25 November 2015.
  14. ↑ Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming . 3 (3): 237–258. arXiv: cs/9301104 . doi:10.1016/0743-1066(86)90015-4. S2CID   27085090.
  15. ↑ Paulson, Lawrence C. (1998). "The inductive approach to verifying cryptographic protocols". Journal of Computer Security. 6 (1–2): 85–128. arXiv: 2105.06319 . CiteSeerX   10.1.1.57.2049 . doi:10.3233/JCS-1998-61-205. ISSN   1875-8924. S2CID   7591720.
  16. ↑ Paulson, L. C. (2012). "Meti Tarski: Past and Future". Interactive Theorem Proving. Lecture Notes in Computer Science. Vol. 7406. pp. 1–10. CiteSeerX   10.1.1.259.5577 . doi:10.1007/978-3-642-32347-8_1. ISBN   978-3-642-32346-1.
  17. ↑ Paulson, Larry. "Logic and Proof". University of Cambridge. Retrieved 27 January 2020.
  18. ↑ Paulson, Larry. "Foundations of Computer Science" . Retrieved 25 November 2015.
  19. ↑ "Department of Computer Science and Technology – Course pages 2017–18: Foundations of Computer Science". www.cl.cam.ac.uk. Retrieved 27 January 2020.
  20. ↑ "Department of Computer Science and Technology – Course pages 2019–20: Foundations of Computer Science". www.cl.cam.ac.uk. Retrieved 27 January 2020.
  21. ↑ "Certificate of Appointment" (PDF). TU Munich. Retrieved 12 April 2016.
  22. ↑ Paulson, Lawrence (2010). "Susan Paulson, PhD (1959–2010)". University of Cambridge. Retrieved 25 November 2015.


This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.