Lawrence Paulson
| Lawrence Paulson | |
|---|---|
| Born |
Lawrence Charles Paulson 1955 (age 60–61) |
| Citizenship | US/UK |
| Fields | |
| Institutions | University of Cambridge |
| Alma mater | |
| Thesis | A Compiler Generator for Semantic Grammars (1981) |
| Doctoral advisor | John L. Hennessy[2] |
| Doctoral students | |
| Known for | |
| Notable awards |
|
| Spouse |
|
|
Website www | |
Lawrence Charles Paulson (born 1955) is a professor at the University of Cambridge Computer Laboratory and a fellow of Clare College, Cambridge.[1][2][6][7][8][9]
Education
Paulson graduated from the California Institute of Technology in 1977, and obtained his PhD in Computer Science from Stanford University under the supervision of John L. Hennessy.[2][10]
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.[11][12] His research is based around the interactive theorem prover Isabelle, which he introduced in 1986.[13] 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,[5] for real-valued special functions.[14]
Teaching
Paulson teaches two undergraduate lecture courses on the Computer Science Tripos, entitled Foundations of Computer Science[15] (which introduces functional programming) and Logic and Proof[16](which covers automated theorem proving and related methods).
Personal life
Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010.[17] He is now married to Dr Elena Tchougounova.
Awards and honours
Paulson is a Fellow of the Association for Computing Machinery (2008).
References
- 1 2 Lawrence Paulson's publications indexed by Google Scholar, a service provided by Google
- 1 2 3 4 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.
- 1 2 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 Association for Computing Machinery (ACM) Digital Library
- ↑ Lawrence Paulson's publications indexed by the DBLP Bibliography Server at the University of Trier
- ↑ Lawrence Paulson's publications indexed by the Scopus bibliographic database, a service provided by Elsevier.
- ↑ Paulson, Lawrence Charles (1981). A Compiler Generator for Semantic Grammars (PhD thesis). Stanford University.
- ↑ 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, 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.
- ↑ "Susan Paulson, PhD (1959–2010)". Retrieved 25 November 2015.
|