Lawrence Paulson at the Royal Society admissions day in London, July 2017
Lawrence Charles Paulson
1955 (age 63–64)
|Institutions||University of Cambridge|
Technical University of Munich
|Thesis||A Compiler Generator for Semantic Grammars (1981)|
|Doctoral advisor||John L. Hennessy|
Paulson graduated from the California Institute of Technology in 1977, 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.
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. His research is based around the interactive theorem prover Isabelle, which he introduced in 1986. He has worked on the verification of cryptographic protocols using inductive definitions, and he has also formalised the constructible universe of Kurt Gödel. Recently he has built a new theorem prover, MetiTarski, for real-valued special functions.
Paulson teaches two undergraduate lecture courses on the Computer Science Tripos, entitled Foundations of Computer Science (which introduces functional programming) and Logic and Proof (which covers automated theorem proving and related methods). His former doctoral students include Jacques Fleuriot Florian Kammüller and David Wolfram.
Awards and honours
Paulson was elected a Fellow of the Royal Society (FRS) in 2017, a Fellow of the Association for Computing Machinery in 2008 and a Distinguished Affiliated Professor for Logic in Informatics at the Technical University of Munich.[when?]
- Anon (2017). Paulson, Prof. Lawrence Charles. ukwhoswho.com. Who's Who (online Oxford University Press ed.). A & C Black, an imprint of Bloomsbury Publishing plc. doi:10.1093/ww/9780199540884.013.289302. (subscription required)
- Anon (2017). "Professor Lawrence Paulson FRS". royalsociety.org. London: Royal Society. Retrieved 5 May 2017.
- 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.
- Anon (2008). "Professor Lawrence C. Paulson". awards.acm.org. Association for Computing Machinery. Retrieved 12 April 2016.
- Lawrence Paulson publications indexed by Google Scholar
- Lawrence Paulson at the Mathematics Genealogy Project
- Lawrence Paulson author profile page at the ACM Digital Library
- Lawrence C. Paulson at DBLP Bibliography Server
- Lawrence Paulson publications indexed by the Scopus bibliographic database. (subscription required)
- Lawrence Paulson Entry at ORCID
- Paulson, Lawrence Charles (1981). A Compiler Generator for Semantic Grammars (PDF). cl.cam.ac.uk (PhD thesis). Stanford University. OCLC 757240716.
- 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. doi:10.1016/0743-1066(86)90015-4.
- Paulson, Lawrence C. (1998). "The inductive approach to verifying cryptographic protocols". Journal of Computer Security. 6 (1–2): 85–128. CiteSeerX 10.1.1.57.2049. doi:10.3233/JCS-1998-61-205. ISSN 1875-8924.
- Paulson, L. C. (2012). "Meti Tarski: Past and Future". Interactive Theorem Proving. Lecture Notes in Computer Science. 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. "Foundations of Computer Science". Retrieved 25 November 2015.
- Paulson, Larry. "Logic and Proof". University of Cambridge. Retrieved 25 November 2015.
- Fleuriot, Jacques Désiré (1990). A combination of geometry theorem proving and nonstandard analysis, with application to Newton's Principia. lib.cam.ac.uk (PhD thesis). University of Cambridge. OCLC 964354126. EThOS uk.bl.ethos.624342.
- Kammüller, Florian (1999). Modular reasoning in Isabelle. lib.cam.ac.uk (PhD thesis). University of Cambridge. OCLC 43649212. EThOS uk.bl.ethos.624446.
- Wolfram, David (1990). The Clausal Theory of Types. lib.cam.ac.uk (PhD thesis). University of Cambridge. OCLC 59897938. EThOS uk.bl.ethos.358763.
- "Certificate of Appointment" (PDF). TU Munich. Retrieved 12 April 2016.
- Paulson, Laurence (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.|