Lawrence Paulson
American computer scientist
From Wikipedia, the free encyclopedia
Lawrence Charles Paulson is an American computer scientist. He 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]
1955 (age 70–71)[1]
Lawrence Paulson | |
|---|---|
Paulson in 2017 | |
| Born | Lawrence Charles Paulson 1955 (age 70–71)[1] |
| Citizenship | US/UK |
| Alma mater | |
| Known for | |
| Spouses |
|
| 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 | Official website  |
Education
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
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 taught an undergraduate lecture course in the Computer Science Tripos, entitled Logic and Proof[17] which covers automated theorem proving and related methods. He also used to teach Foundations of Computer Science[18] which introduces functional programming, but this course was taken over by Alan Mycroft and Amanda Prorok in 2017,[19] and then Anil Madhavapeddy and Amanda Prorok in 2019.[20]
Awards and honours
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?][21]
