Lawrence Paulson

Lawrence Paulson FRS
Lawrence Paulson at the Royal Society admissions day in London, July 2017
Born	Lawrence Charles Paulson 1955 (age 68–69)^[4]
Citizenship	US/UK
Alma mater	California Institute of Technology (BSc) Stanford University (PhD)
Known for	ML Isabelle^[5] MetiTarski^[6]
Spouses	Susan Mary Paulson (d. 2010) Elena Tchougounova
Awards	ACM Fellow (2008)^[1]
Scientific career
Fields	Theorem proving^[2] Formal methods^[2] Computer security^[2]
Institutions	University of Cambridge Technical University of Munich
Thesis	A Compiler Generator for Semantic Grammars (1981)
Doctoral advisor	John L. Hennessy^[3]

Website	www.cl.cam.ac.uk/~lp15/

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 universeofKurt 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])

^ ^a ^b ^c ^d Lawrence Paulson publications indexed by Google Scholar

^ ^a ^b ^c Anon (2017). "Professor Lawrence Paulson FRS". royalsociety.org. London: Royal Society. Retrieved 5 May 2017.

^ ^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.

^ Lawrence Paulson author profile page at the ACM Digital Library

^ Lawrence C. PaulsonatDBLP Bibliography Server

^ Lawrence Paulson publications indexed by the Scopus bibliographic database. (subscription required)

^ Paulson, Lawrence (1996). ML for the working programmer. Cambridge New York: Cambridge University Press. ISBN 978-0521565431.

^ "ML for the Working Programmer". University of Cambridge. Retrieved 25 November 2015.

^ 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.

^ 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.

^ 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.

^ Paulson, Larry. "Logic and Proof". University of Cambridge. Retrieved 27 January 2020.

^ Paulson, Larry. "Foundations of Computer Science". Retrieved 25 November 2015.

^ "Certificate of Appointment" (PDF). TU Munich. Retrieved 12 April 2016.

^ Paulson, Lawrence (2010). "Susan Paulson, PhD (1959–2010)". University of Cambridge. Retrieved 25 November 2015.

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

Contents