Lawrence Paulson
Lawrence Paulson | |
---|---|
Born | Lawrence Charles Paulson 1955 (age 68–69) |
Citizenship | US/UK |
Fields | <templatestyles src="Plainlist/styles.css"/> |
Institutions | University of Cambridge |
Alma mater | <templatestyles src="Plainlist/styles.css"/> |
Thesis | A Compiler Generator for Semantic Grammars (1981) |
Doctoral advisor | John L. Hennessy[2] |
Doctoral students | <templatestyles src="Plainlist/styles.css"/>
|
Known for | <templatestyles src="Plainlist/styles.css"/> |
Notable awards | <templatestyles src="Plainlist/styles.css"/>
|
Spouse | <templatestyles src="Plainlist/styles.css"/>
|
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.0 1.1 Lawrence Paulson's publications indexed by Google Scholar, a service provided by Google
- ↑ 2.0 2.1 2.2 2.3 Lawrence Paulson at the Mathematics Genealogy Project
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ 5.0 5.1 Lua error in package.lua at line 80: module 'strict' not found.
- ↑ 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.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
Lua error in package.lua at line 80: module 'strict' not found.
<templatestyles src="Asbox/styles.css"></templatestyles>
- Articles with unsourced statements from March 2014
- 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
- Formal methods people
- Computer specialist stubs