Lawrence Paulson | |
---|---|
![]() Lawrence Paulson at the
Royal Society admissions day in London, July 2017 | |
Born | Lawrence Charles Paulson 1955 (age 68–69) [4] |
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 [3] |
Website |
www |
Lawrence Charles Paulson FRS [5] (born 1955) [4] 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. [2] [3] [7] [8] [9]
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. [3] [11]
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, [6] for real-valued special functions. [16]
Paulson teaches an undergraduate lecture course in the Computer Science Tripos, entitled Logic and Proof [17] which covers automated theorem proving and related methods. (He 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])
Paulson was elected a Fellow of the Royal Society (FRS) in 2017, [5] a Fellow of the Association for Computing Machinery in 2008 [1] and a Distinguished Affiliated Professor for Logic in Informatics at the Technical University of Munich.[ when?] [21]
Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010. [22] Since 2012, he has been married to Dr Elena Tchougounova. [4]
Lawrence Paulson | |
---|---|
![]() Lawrence Paulson at the
Royal Society admissions day in London, July 2017 | |
Born | Lawrence Charles Paulson 1955 (age 68–69) [4] |
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 [3] |
Website |
www |
Lawrence Charles Paulson FRS [5] (born 1955) [4] 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. [2] [3] [7] [8] [9]
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. [3] [11]
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, [6] for real-valued special functions. [16]
Paulson teaches an undergraduate lecture course in the Computer Science Tripos, entitled Logic and Proof [17] which covers automated theorem proving and related methods. (He 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])
Paulson was elected a Fellow of the Royal Society (FRS) in 2017, [5] a Fellow of the Association for Computing Machinery in 2008 [1] and a Distinguished Affiliated Professor for Logic in Informatics at the Technical University of Munich.[ when?] [21]
Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010. [22] Since 2012, he has been married to Dr Elena Tchougounova. [4]