Jump to content

Lawrence Paulson: Difference between revisions

From Wikipedia, the free encyclopedia
Browse history interactively
← Previous editNext edit →
Content deleted Content added
VisualWikitext
refs
Corrected parameter for Template:AcademicSearch
Line 27: Line 27:
|academic_advisors =
|academic_advisors =
|doctoral_students = {{Plainlist|
|doctoral_students = {{Plainlist|
* Jacques Fleuriot<ref name="fleuriotphd">{{cite thesis |degree=PhD |first= Jacques Désiré|last= Fleuriot |title=A combination of geometry theorem proving and nonstandard analysis, with application to Newton's Principia |publisher=University of Cambridge |date=1990 |url=http://ulmss-newton.lib.cam.ac.uk/vwebv/holdingsInfo?bibId=20998}}</ref>
* Jacques Fleuriot{{fact}}
* Florian Kammueller{{fact}}
* Florian Kammueller{{fact}}
* David Wolfram<ref name="wolfphd">{{cite thesis |degree=PhD |first=David|last=Wolfram |title=The Clausal Theory of Types |publisher=University of Cambridge |date=1990 |url=http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.358763}}</ref><ref name="mathgene"/>}}
* David Wolfram<ref name="mathgene"/><ref name="wolfphd">{{cite thesis |degree=PhD |first=David|last=Wolfram |title=The Clausal Theory of Types |publisher=University of Cambridge |date=1990 |url=http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.358763}}</ref>}}
|notable_students =
|notable_students =
|known_for = {{Plainlist|
|known_for = {{Plainlist|
Line 47: Line 47:
|footnotes =
|footnotes =
| website = {{URL|http://www.cl.cam.ac.uk/~lp15/}}
| website = {{URL|http://www.cl.cam.ac.uk/~lp15/}}
}}'''Lawrence Charles Paulson''' (born 1955) is a professor at the [[University of Cambridge]] [[University of Cambridge Computer Laboratory|Computer Laboratory]] and a fellow of [[Clare College, Cambridge]].<ref name="microsoft">{{AcademicSearch| 1363468}}</ref><ref name="acm">{{ACMPortal|id= 81100146628}}</ref><ref name="dblp">{{DBLP|id=Paulson:Lawrence_C=}}</ref><ref name="googlescholar">{{GoogleScholar|Sv1hcjEAAAAJ}}</ref><ref name="mathgene">{{MathGenealogy|id= 25162}}</ref><ref name="scopus">{{Scopus|id= 7005293178}}</ref>
}}'''Lawrence Charles Paulson''' (born 1955) is a professor at the [[University of Cambridge]] [[University of Cambridge Computer Laboratory|Computer Laboratory]] and a fellow of [[Clare College, Cambridge]].<ref name="microsoft">{{AcademicSearch|1363468}}</ref><ref name="acm">{{ACMPortal|id=81100146628}}</ref><ref name="dblp">{{DBLP|id=Paulson:Lawrence_C=}}</ref><ref name="googlescholar">{{GoogleScholar|Sv1hcjEAAAAJ}}</ref><ref name="mathgene">{{MathGenealogy|id= 25162}}</ref><ref name="scopus">{{Scopus|id= 7005293178}}</ref>


==Education==
==Education==
Line 53: Line 53:


==Research==
==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 (programming language)|ML]], ''ML for the Working Programmer'' <ref>{{cite isbn|052156543X}}</ref><ref>http://www.cl.cam.ac.uk/users/lcp/MLbook</ref>. His research is based around the interactive theorem prover [[Isabelle theorem prover|Isabelle]], which he introduced in 1986. He has worked on the verification of [[cryptography|cryptographic protocols]] using [[inductive definition]]s, and he has also formalized the [[constructible universe]] of [[Kurt Gödel]]. Recently he has built a new theorem prover, MetiTarski,<ref name="metitarski"/> for real-valued special functions.
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 (programming language)|ML]], ''ML for the Working Programmer'' <ref>{{cite isbn|052156543X}}</ref><ref>http://www.cl.cam.ac.uk/users/lcp/MLbook</ref>. His research is based around the interactive theorem prover [[Isabelle theorem prover|Isabelle]], which he introduced in 1986.{{fact}} He has worked on the verification of [[cryptography|cryptographic protocols]] using [[inductive definition]]s, and he has also formalized the [[constructible universe]] of [[Kurt Gödel]]. Recently he has built a new theorem prover, MetiTarski,<ref name="metitarski"/> for real-valued special functions.<ref>{{cite doi|10.1007/978-3-642-32347-8_1|noedit}}</ref>


==Teaching==
==Teaching==

Revision as of 23:19, 25 March 2014

Lawrence Paulson
Born
Lawrence Charles Paulson

1955 (age 68–69)
CitizenshipUS/UK
Alma mater
Known for
Spouses
  • Susan Mary Paulson (d. 2010)
  • Elena Tchougounova
Awards
  • Pilkington Teaching Prize (2003)
  • FACM (2008)
Scientific career
Fields
InstitutionsUniversity of Cambridge
ThesisA Compiler Generator for Semantic Grammars (1981)
Doctoral advisorJohn L. Hennessy[2]
Doctoral students
Websitewww.cl.cam.ac.uk/~lp15/

Lawrence Charles Paulson (born 1955) is a professor at the University of Cambridge Computer Laboratory and a fellow of Clare College, Cambridge.[6][7][8][1][2][9]

Education

Paulson graduated from the California Institute of Technology in 1977, and obtained his PhD in Computer Science from Stanford University under the supervision of John L. Hennessy.[10][2]

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 [11][12]. His research is based around the interactive theorem prover Isabelle, which he introduced in 1986.[citation needed] He has worked on the verification of cryptographic protocols using inductive definitions, and he has also formalized the constructible universe of Kurt Gödel. Recently he has built a new theorem prover, MetiTarski,[5] for real-valued special functions.[13]

Teaching

Paulson teaches two undergraduate lecture courses on the Computer Science Tripos, entitled Foundations of Computer Science (which introduces functional programming) and Logic and Proof (which covers automated theorem proving and related methods).[citation needed]

Personal life

Paulson has two children by his first wife, Dr Susan Mary Paulson, who died 2010. He is now married to Dr Elena Tchougounova.

Awards and honours

Paulson is a Fellow of the Association for Computing Machinery (2008).

References

  1. ^ a b Lawrence Paulson publications indexed by Google Scholar
  2. ^ a b c d Lawrence Paulson at the Mathematics Genealogy Project
  3. ^ Fleuriot, Jacques Désiré (1990). A combination of geometry theorem proving and nonstandard analysis, with application to Newton's Principia (PhD thesis). University of Cambridge.
  4. ^ Wolfram, David (1990). The Clausal Theory of Types (PhD thesis). University of Cambridge.
  5. ^ a b Attention: This template ({{cite doi}}) is deprecated. To cite the publication identified by doi:10.1007/s10817-009-9149-2, please use {{cite journal}} (if it was published in a bona fide academic journal, otherwise {{cite report}} with |doi=10.1007/s10817-009-9149-2 instead.
  6. ^ Lawrence Paulson publications indexed by Microsoft Academic
  7. ^ Lawrence Paulson author profile page at the ACM Digital Library
  8. ^ Lawrence Paulson at DBLP Bibliography Server Edit this at Wikidata
  9. ^ Lawrence Paulson's publications indexed by the Scopus bibliographic database. (subscription required)
  10. ^ Paulson, Lawrence Charles (1981). A Compiler Generator for Semantic Grammars (PhD thesis). Stanford University.
  11. ^ Template:Cite isbn
  12. ^ http://www.cl.cam.ac.uk/users/lcp/MLbook
  13. ^ Attention: This template ({{cite doi}}) is deprecated. To cite the publication identified by doi:10.1007/978-3-642-32347-8_1, please use {{cite journal}} (if it was published in a bona fide academic journal, otherwise {{cite report}} with |doi=10.1007/978-3-642-32347-8_1 instead.

Template:Persondata


Stub icon

This biographical article relating to a computer specialist is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Lawrence_Paulson&oldid=601269711"