|Born||Lawrence Charles Paulson
1955 (age 58–59)
|Institutions||University of Cambridge|
|Thesis||A Compiler Generator for Semantic Grammars (1981)|
|Doctoral advisor||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 formalized 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).
Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010. He is now married to Dr Elena Tchougounova.
Awards and honours
Paulson is a Fellow of the Association for Computing Machinery (2008).
- List of publications from Google Scholar
- Lawrence Paulson at the Mathematics Genealogy Project
- Fleuriot, Jacques Désiré (1990). A combination of geometry theorem proving and nonstandard analysis, with application to Newton's Principia (PhD thesis). University of Cambridge.
- Wolfram, David (1990). The Clausal Theory of Types (PhD thesis). University of Cambridge.
- 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.
- List of publications from Microsoft Academic Search
- Lawrence Paulson from the ACM Portal
- List of publications from the DBLP Bibliography Server
- Lawrence Paulson from the Scopus bibliographic database.
- Paulson, Lawrence Charles (1981). A Compiler Generator for Semantic Grammars (PhD thesis). Stanford University.
- ISBN 052156543X
- 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, 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.
|This biographical article relating to a computer specialist is a stub. You can help Wikipedia by expanding it.|