Lawrence Paulson
Lawrence Paulson | |
---|---|
Lawrence Paulson at the Royal Society admissions day in London, July 2017 | |
Born | Lawrence Charles Paulson 1955 (age 63–64)[1] |
Citizenship | US/UK |
Alma mater | |
Known for | |
Spouse(s) |
|
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 |
Lawrence Charles Paulson (born 1955)[1] FRS[2] 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]
Education[edit]
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[edit]
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 teaches two undergraduate lecture courses on the Computer Science Tripos, entitled Foundations of Computer Science[17] (which introduces functional programming) and Logic and Proof[18] (which covers automated theorem proving and related methods). His former doctoral students include Jacques Fleuriot[6][19] Florian Kammüller[6][20] and David Wolfram.[6][21]
Awards and honours[edit]
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?][22]
Personal life[edit]
Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010.[23] Since 2012, he has been married to Dr Elena Tchougounova.[1]
References[edit]
- ^ a b c 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)
- ^ 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. doi:10.1007/s10817-009-9149-2.
- ^ a b Anon (2008). "Professor Lawrence C. Paulson". awards.acm.org. Association for Computing Machinery. Retrieved 12 April 2016.
- ^ a b c d Lawrence Paulson publications indexed by Google Scholar
- ^ a b c d e f 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 052156543X.
- ^ "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. 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. 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. p. 1. 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. |
- 1955 births
- Living people
- American computer scientists
- Members of the University of Cambridge Computer Laboratory
- California Institute of Technology alumni
- Stanford University alumni
- Fellows of Clare College, Cambridge
- Fellows of the Association for Computing Machinery
- Fellows of the Royal Society
- Formal methods people
- Computer specialist stubs