Jump to content

Lawrence Paulson

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by Trappist the monk (talk | contribs) at 19:30, 6 August 2023 (→top: replace to-be-deprecated parameters;). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Lawrence Paulson
FRS
Lawrence Paulson at the Royal Society admissions day in London, July 2017
Born
Lawrence Charles Paulson

1955 (age 68–69)[4]
CitizenshipUS/UK
Alma mater
Known for
Spouses
  • Susan Mary Paulson (d. 2010)
  • Elena Tchougounova
Awards
Scientific career
Fields
InstitutionsUniversity of Cambridge
Technical University of Munich
ThesisA Compiler Generator for Semantic Grammars (1981)
Doctoral advisorJohn L. Hennessy[3]
Websitewww.cl.cam.ac.uk/~lp15/

Lawrence Charles Paulson FRS[5] (born 1955)[4] 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.[2][3][7][8][9]

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.[3][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,[6] for real-valued 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])

Awards and honours

Paulson was elected a Fellow of the Royal Society (FRS) in 2017,[5] a Fellow of the Association for Computing Machinery in 2008[1] 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.[4]

References

  1. ^ a b Anon (2008). "Professor Lawrence C. Paulson". awards.acm.org. Association for Computing Machinery. Retrieved 12 April 2016.
  2. ^ a b c d Lawrence Paulson publications indexed by Google Scholar Edit this at Wikidata
  3. ^ a b c Lawrence Paulson at the Mathematics Genealogy Project
  4. ^ a b c 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.)
  5. ^ a b c Anon (2017). "Professor Lawrence Paulson FRS". royalsociety.org. London: Royal Society. Retrieved 5 May 2017.
  6. ^ 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. CiteSeerX 10.1.1.157.3300. doi:10.1007/s10817-009-9149-2. S2CID 16215962.
  7. ^ Lawrence Paulson author profile page at the ACM Digital Library
  8. ^ Lawrence C. Paulson at DBLP Bibliography Server Edit this at Wikidata
  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.


Stub icon

This biographical article relating to a computer specialist is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Lawrence_Paulson&oldid=1169052907"