Lawrence Paulson
Encyclopedia
Lawrence Charles Paulson (born 1955) is a professor at the University of Cambridge
Computer Laboratory
and a fellow of Clare College
. He lectures courses on the foundations of computer science
, logic
and proof
among others. He is best known for the cornerstone text on the programming language ML, ML for the Working Programmer http://www.cl.cam.ac.uk/users/lcp/MLbook. His research is based around the interactive theorem prover Isabelle
. He has worked on the verification of cryptographic protocols
using inductive definitions, and he has also formalized the constructible universe
of Kurt Gödel
. Current research projects are described on his web page.
Paulson graduated from the California Institute of Technology
in 1977, and obtained his PhD in Computer Science from Stanford University
. He came to the University of Cambridge in 1983 and became a fellow in 1987. He is widowed, with two children.
He is a Fellow of the Association for Computing Machinery
(2008).
University of Cambridge
The University of Cambridge is a public research university located in Cambridge, United Kingdom. It is the second-oldest university in both the United Kingdom and the English-speaking world , and the seventh-oldest globally...
Computer Laboratory
University of Cambridge Computer Laboratory
The Computer Laboratory is the computer science department of the University of Cambridge. As of 2007, it employs 35 academic staff, 25 support staff, 35 affiliated research staff, and about 155 research students...
and a fellow of Clare College
Clare College, Cambridge
Clare College is a constituent college of the University of Cambridge in Cambridge, England.The college was founded in 1326, making it the second-oldest surviving college of the University after Peterhouse. Clare is famous for its chapel choir and for its gardens on "the Backs"...
. He lectures courses on the foundations of computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
and proof
Proof
Proof may refer to:* Proof , sufficient evidence or argument for the truth of a proposition* Formal proof* Mathematical proof, a convincing demonstration that some mathematical statement is necessarily true...
among others. He is best known for the cornerstone text on the programming language ML, ML for the Working Programmer http://www.cl.cam.ac.uk/users/lcp/MLbook. His research is based around the interactive theorem prover Isabelle
Isabelle theorem prover
The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic theorem prover. It is an LCF-style theorem prover , so it is based on a small logical core guaranteeing logical correctness...
. He has worked on the verification of cryptographic protocols
Cryptography
Cryptography is the practice and study of techniques for secure communication in the presence of third parties...
using inductive definitions, and he has also formalized the constructible universe
Constructible universe
In mathematics, the constructible universe , denoted L, is a particular class of sets which can be described entirely in terms of simpler sets. It was introduced by Kurt Gödel in his 1938 paper "The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis"...
of Kurt Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
. Current research projects are described on his web page.
Paulson graduated from the California Institute of Technology
California Institute of Technology
The California Institute of Technology is a private research university located in Pasadena, California, United States. Caltech has six academic divisions with strong emphases on science and engineering...
in 1977, and obtained his PhD in Computer Science from Stanford University
Stanford University
The Leland Stanford Junior University, commonly referred to as Stanford University or Stanford, is a private research university on an campus located near Palo Alto, California. It is situated in the northwestern Santa Clara Valley on the San Francisco Peninsula, approximately northwest of San...
. He came to the University of Cambridge in 1983 and became a fellow in 1987. He is widowed, with two children.
He is a Fellow of the Association for Computing Machinery
Association for Computing Machinery
The Association for Computing Machinery is a learned society for computing. It was founded in 1947 as the world's first scientific and educational computing society. Its membership is more than 92,000 as of 2009...
(2008).