Lawrence Paulson

Last updated

Lawrence Paulson
FRS
Lawrence Paulson Royal Society.jpg
Paulson in 2017
Born
Lawrence Charles Paulson

1955 (age 6869) [1]
CitizenshipUS/UK
Alma mater
Known for
Spouses
  • Susan Mary Paulson (d. 2010)
  • Elena Tchougounova
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 www.cl.cam.ac.uk/~lp15/

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]

Contents

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 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] )

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]

Personal life

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. [1]

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major motivating factor for the development of computer science.

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.

The history of logic deals with the study of the development of the science of valid inference (logic). Formal logics developed in ancient times in India, China, and Greece. Greek methods, particularly Aristotelian logic as found in the Organon, found wide application and acceptance in Western science and mathematics for millennia. The Stoics, especially Chrysippus, began the development of predicate logic.

<span class="mw-page-title-main">Robin Milner</span> British computer scientist (1934–2010)

Arthur John Robin Gorell Milner was a British computer scientist, and a Turing Award winner.

<span class="mw-page-title-main">Isabelle (proof assistant)</span> Higher-order logic (HOL) automated theorem prover

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.

HOL denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defines an abstract data type of proven theorems such that new objects of this type can only be created using the functions in the library which correspond to inference rules in higher-order logic. As long as these functions are correctly implemented, all theorems proven in the system must be valid. As such, a large system can be built on top of a small trusted kernel.

Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general-purpose programming language ML to allow users to write theorem-proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions.

E is a high-performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E is developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich, now at Baden-Württemberg Cooperative State University Stuttgart.

<span class="mw-page-title-main">Department of Computer Science and Technology, University of Cambridge</span> Computer science division at the University of Cambridge

The Department of Computer Science and Technology, formerly the Computer Laboratory, is the computer science department of the University of Cambridge. As of 2023 it employed 56 faculty members, 45 support staff, 105 research staff, and about 205 research students. The current Head of Department is Professor Alastair Beresford.

<span class="mw-page-title-main">Coq (software)</span> Proof assistant

Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer. Zeroth-order logic is decidable, whereas first-order and higher-order logic are not. Logical systems are decidable if membership in their set of logically valid formulas can be effectively determined. A theory in a fixed logical system is decidable if there is an effective method for determining whether arbitrary formulas are included in the theory. Many important problems are undecidable, that is, it has been proven that no effective method for determining membership can exist for them.

<span class="mw-page-title-main">Proof assistant</span> Software tool to assist with the development of formal proofs by human–machine collaboration

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

Patrick John Hayes FAAAI is a British computer scientist who lives and works in the United States. As of March 2006, he is a senior research scientist at the Institute for Human and Machine Cognition in Pensacola, Florida.

<span class="mw-page-title-main">Michael J. C. Gordon</span> British computer scientist

Michael John Caldwell Gordon was a British computer scientist.

In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.

In mathematics and abstract algebra, a relation algebra is a residuated Boolean algebra expanded with an involution called converse, a unary operation. The motivating example of a relation algebra is the algebra 2X 2 of all binary relations on a set X, that is, subsets of the cartesian square X2, with RS interpreted as the usual composition of binary relations R and S, and with the converse of R as the converse relation.

<span class="mw-page-title-main">Jeff Paris (mathematician)</span> British mathematician (born 1944)

Jeffrey Bruce Paris is a British mathematician and Professor of Logic in the School of Mathematics at the University of Manchester.

<span class="mw-page-title-main">Peter Aczel</span> British mathematician and logician

Peter Henry George Aczel was a British mathematician, logician and Emeritus joint Professor in the Department of Computer Science and the School of Mathematics at the University of Manchester. He is known for his work in non-well-founded set theory, constructive set theory, and Frege structures.

Inductive programming (IP) is a special area of automatic programming, covering research from artificial intelligence and programming, which addresses learning of typically declarative and often recursive programs from incomplete specifications, such as input/output examples or constraints.

In mathematical logic, a first-order language of the real numbers is the set of all well-formed sentences of first-order logic that involve universal and existential quantifiers and logical combinations of equalities and inequalities of expressions over real variables. The corresponding first-order theory is the set of sentences that are actually true of the real numbers. There are several different such theories, with different expressive power, depending on the primitive operations that are allowed to be used in the expression. A fundamental question in the study of these theories is whether they are decidable: that is, whether there is an algorithm that can take a sentence as input and produce as output an answer "yes" or "no" to the question of whether the sentence is true in the theory.

References

  1. 1 2 Anon (2017). "Paulson, Prof. Lawrence Charles" . Who's Who (online Oxford University Press  ed.). Oxford: A & C Black. doi:10.1093/ww/9780199540884.013.289302.(Subscription or UK public library membership required.)
  2. 1 2 Anon (2017). "Professor Lawrence Paulson FRS". royalsociety.org. London: Royal Society . Retrieved 5 May 2017.
  3. 1 2 Akbarpour, B.; Paulson, L. C. (2009). "Meti Tarski: An Automatic Theorem Prover for Real-Valued Special Functions". Journal of Automated Reasoning . 44 (3): 175. CiteSeerX   10.1.1.157.3300 . doi:10.1007/s10817-009-9149-2. S2CID   16215962.
  4. 1 2 Anon (2008). "Professor Lawrence C. Paulson". awards.acm.org. Association for Computing Machinery . Retrieved 12 April 2016.
  5. 1 2 3 4 Lawrence Paulson publications indexed by Google Scholar OOjs UI icon edit-ltr-progressive.svg
  6. 1 2 3 Lawrence Paulson at the Mathematics Genealogy Project
  7. Lawrence Paulson author profile page at the ACM Digital Library
  8. Lawrence C. Paulson at DBLP Bibliography Server OOjs UI icon edit-ltr-progressive.svg
  9. Lawrence Paulson publications indexed by the Scopus bibliographic database. (subscription required)
  10. Lawrence Paulson ORCID   0000-0003-0288-4279
  11. Paulson, Lawrence Charles (1981). A Compiler Generator for Semantic Grammars (PDF). cl.cam.ac.uk (PhD thesis). Stanford University. OCLC   757240716.
  12. Paulson, Lawrence (1996). ML for the working programmer. Cambridge New York: Cambridge University Press. ISBN   978-0521565431.
  13. "ML for the Working Programmer". University of Cambridge. Retrieved 25 November 2015.
  14. Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming . 3 (3): 237–258. arXiv: cs/9301104 . doi:10.1016/0743-1066(86)90015-4. S2CID   27085090.
  15. Paulson, Lawrence C. (1998). "The inductive approach to verifying cryptographic protocols". Journal of Computer Security. 6 (1–2): 85–128. arXiv: 2105.06319 . CiteSeerX   10.1.1.57.2049 . doi:10.3233/JCS-1998-61-205. ISSN   1875-8924. S2CID   7591720.
  16. Paulson, L. C. (2012). "Meti Tarski: Past and Future". Interactive Theorem Proving. Lecture Notes in Computer Science. Vol. 7406. pp. 1–10. CiteSeerX   10.1.1.259.5577 . doi:10.1007/978-3-642-32347-8_1. ISBN   978-3-642-32346-1.
  17. Paulson, Larry. "Logic and Proof". University of Cambridge. Retrieved 27 January 2020.
  18. Paulson, Larry. "Foundations of Computer Science" . Retrieved 25 November 2015.
  19. "Department of Computer Science and Technology – Course pages 2017–18: Foundations of Computer Science". www.cl.cam.ac.uk. Retrieved 27 January 2020.
  20. "Department of Computer Science and Technology – Course pages 2019–20: Foundations of Computer Science". www.cl.cam.ac.uk. Retrieved 27 January 2020.
  21. "Certificate of Appointment" (PDF). TU Munich. Retrieved 12 April 2016.
  22. Paulson, Lawrence (2010). "Susan Paulson, PhD (1959–2010)". University of Cambridge. Retrieved 25 November 2015.