HOME

TheInfoList



OR:

Lawrence Charles Paulson (born 1955) is an American
computer scientist A computer scientist is a person who is trained in the academic study of computer science. Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (a ...
. He is a
Professor Professor (commonly abbreviated as Prof.) is an academic rank at universities and other post-secondary education and research institutions in most countries. Literally, ''professor'' derives from Latin as a "person who professes". Professo ...
of
Computational Logic Computational logic is the use of logic to perform or reason about computation. It bears a similar relationship to computer science and engineering as mathematical logic bears to mathematics and as philosophical logic bears to philosophy. It is s ...
at the
University of Cambridge Computer Laboratory The Department of Computer Science and Technology, formerly the Computer Laboratory, is the computer science department of the University of Cambridge. it employed 35 academic staff, 25 support staff, 35 affiliated research staff, and about 15 ...
and a
Fellow A fellow is a concept whose exact meaning depends on context. In learned or professional societies, it refers to a privileged member who is specially elected in recognition of their work and achievements. Within the context of higher education ...
of
Clare College, Cambridge Clare College is a constituent college of the University of Cambridge in Cambridge, England. The college was founded in 1326 as University Hall, making it the second-oldest surviving college of the University after Peterhouse. It was refound ...
.


Education

Paulson graduated from the
California Institute of Technology The California Institute of Technology (branded as Caltech or CIT)The university itself only spells its short form as "Caltech"; the institution considers other spellings such a"Cal Tech" and "CalTech" incorrect. The institute is also occasional ...
in 1977,Lawrence Paulson and obtained his PhD in Computer Science from
Stanford University Stanford University, officially Leland Stanford Junior University, is a private research university in Stanford, California. The campus occupies , among the largest in the United States, and enrolls over 17,000 students. Stanford is conside ...
in 1981 for research on
programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...
s and
compiler-compiler In computer science, a compiler-compiler or compiler generator is a programming tool that creates a parser, interpreter, or compiler from some form of formal description of a programming language and machine. The most common type of compiler ...
s supervised by
John L. Hennessy John Leroy Hennessy (born September 22, 1952) is an American computer scientist, academician and businessman who serves as Chairman of Alphabet Inc. Hennessy is one of the founders of MIPS Computer Systems Inc. as well as Atheros and served as ...
.


Research

Paulson came to the
University of Cambridge , mottoeng = Literal: From here, light and sacred draughts. Non literal: From this place, we gain enlightenment and precious knowledge. , established = , other_name = The Chancellor, Masters and Schola ...
in 1983 and became a Fellow of
Clare College, Cambridge Clare College is a constituent college of the University of Cambridge in Cambridge, England. The college was founded in 1326 as University Hall, making it the second-oldest surviving college of the University after Peterhouse. It was refound ...
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 Isabel is a female name of Spanish origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of ''Elizabeth (given name), Elisabeth'' (ultimately Hebrew ''Elisheba, Elisheva''), Arising in ...
, which he introduced in 1986. He has worked on the verification of
cryptographic protocols A security protocol (cryptographic protocol or encryption protocol) is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol describ ...
using inductive definitions, and he has also formalised the
constructible universe In mathematics, in set theory, the constructible universe (or Gödel's constructible universe), denoted by , is a particular class of sets that can be described entirely in terms of simpler sets. is the union of the constructible hierarchy . It w ...
of
Kurt Gödel Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imm ...
. Recently he has built a new theorem prover, MetiTarski, for real-valued special functions. Paulson teaches an undergraduate lecture course in the
Computer Science Tripos The Computer Science Tripos (CST) is the undergraduate course in computer science offered by the University of Cambridge Computer Laboratory. It evolved out of the Diploma in Computer Science, the world's first taught course in computer science ...
, entitled ''Logic and Proof'' which covers
automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ...
and related methods. (He used to teach ''Foundations of Computer Science'' which introduces
functional programming In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions tha ...
, but this course was taken over by
Alan Mycroft Alan Mycroft is a professor at the Computer Laboratory, University of Cambridge and a Fellow of Robinson College, Cambridge, where he is also director of studies for computer science. Education Mycroft read mathematics at Cambridge then moved ...
and Amanda Prorok in 2017, and then Anil Madhavapeddy and Amanda Prorok in 2019.)


Awards and honours

Paulson was elected a Fellow of the Royal Society (FRS) in 2017, a Fellow of the Association for Computing Machinery in 2008 and a Distinguished Affiliated Professor for Logic in Informatics at the
Technical University of Munich The Technical University of Munich (TUM or TU Munich; german: Technische Universität München) is a public research university in Munich, Germany. It specializes in engineering, technology, medicine, and applied science, applied and Natural sci ...
.


Personal life

Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010. Since 2012, he has been married to Dr Elena Tchougounova.


References

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 Fellows of the Royal Society Formal methods people {{compu-bio-stub