Lawrence Charles Paulson is an American

computer scientist A computer scientist is a scientist who specializes in the academic study of computer science. Computer scientists typically work on the theoretical side of computation. Although computer scientists can also focus their work and research on ...

. He is a

Professor Professor (commonly abbreviated as Prof.) is an Academy, academic rank at university, universities and other tertiary education, post-secondary education and research institutions in most countries. Literally, ''professor'' derives from Latin ...

of Computational Logic at the University of Cambridge Computer Laboratory and a

Fellow A fellow is a title and form of address for distinguished, learned, or skilled individuals in academia, medicine, research, and industry. The exact meaning of the term differs in each field. In learned society, learned or professional society, p ...

Clare College, Cambridge Clare College is a Colleges of the University of Cambridge, 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 Unive ...

Education

Paulson graduated from the

California Institute of Technology The California Institute of Technology (branded as Caltech) is a private research university in Pasadena, California, United States. The university is responsible for many modern scientific advancements and is among a small group of institutes ...

in 1977,Lawrence Paulson and obtained his PhD in Computer Science from

Stanford University Leland Stanford Junior University, commonly referred to as Stanford University, is a Private university, private research university in Stanford, California, United States. It was founded in 1885 by railroad magnate Leland Stanford (the eighth ...

in 1981 for research on

programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...

s and

compiler-compiler In computer science, a compiler-compiler or compiler generator is a programming tool that creates a Parsing#Computer_languages, parser, interpreter (computer software), interpreter, or compiler from some form of formal description of a programm ...

s supervised by John L. Hennessy.

Research

Paulson came to the

University of Cambridge The University of Cambridge is a Public university, public collegiate university, collegiate research university in Cambridge, England. Founded in 1209, the University of Cambridge is the List of oldest universities in continuous operation, wo ...

in 1983 and became a Fellow of

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, which he introduced in 1986. He has worked on the verification of cryptographic protocols using

inductive definition In mathematics and computer science, a recursive definition, or inductive definition, is used to define the elements in a set in terms of other elements in the set ( Aczel 1977:740ff). Some examples of recursively definable objects include fact ...

s, and he has also formalised the

constructible universe In mathematics, in set theory, the constructible universe (or Gödel's constructible universe), denoted by L, is a particular Class (set theory), class of Set (mathematics), sets that can be described entirely in terms of simpler sets. L is the un ...

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 profoundly ...

. Recently he has built a new theorem prover, MetiTarski, for real-valued special functions. Paulson taught an undergraduate lecture course in the Computer Science Tripos, 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 majo ...

and related methods. He also 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 Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declarat ...

, but this course was taken over by Alan Mycroft 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; ) is a public research university in Munich, Bavaria, Germany. It specializes in engineering, technology, medicine, and applied and natural sciences. Established in 1868 by King Ludwig II ...

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 2008 fellows of the Association for Computing Machinery Fellows of the Royal Society Formal methods people {{compu-bio-stub