Lawrence Paulson

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by Yobot (talk | contribs) at 08:11, 13 April 2016 (→‎Awards and honours: WP:CHECKWIKI error fixes using AWB (12002)). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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.[1][2][6][7][8][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.[2][10]

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.[13] 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.[14]

Teaching

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

Personal life

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

Awards and honours

Paulson is a Fellow of the Association for Computing Machinery (2008)[18] and a Distinguished Affiliated Professor for Logic in Informatics at TU Munich.[19]

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 Akbarpour, B.; Paulson, L. C. (2009). "Meti Tarski: An Automatic Theorem Prover for Real-Valued Special Functions". Journal of Automated Reasoning. 44 (3): 175. doi:10.1007/s10817-009-9149-2.
  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. ^ Paulson, Lawrence (1996). ML for the working programmer. Cambridge New York: Cambridge University Press. ISBN 052156543X.
  12. ^ "ML for the Working Programmer". University of Cambridge. Retrieved 25 November 2015.
  13. ^ Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming. 3 (3): 237. doi:10.1016/0743-1066(86)90015-4.
  14. ^ Paulson, L. C. (2012). "Meti Tarski: Past and Future". Interactive Theorem Proving. Lecture Notes in Computer Science. Vol. 7406. p. 1. doi:10.1007/978-3-642-32347-8_1. ISBN 978-3-642-32346-1.
  15. ^ Paulson, Larry. "Foundations of Computer Science". Retrieved 25 November 2015.
  16. ^ Paulson, Larry. "Logic and Proof". University of Cambridge. Retrieved 25 November 2015.
  17. ^ "Susan Paulson, PhD (1959–2010)". Retrieved 25 November 2015.
  18. ^ "Professor Lawrence C. Paulson". awards.acm.org. Association for Computing Machinery. Retrieved 12 April 2016.
  19. ^ "Certificate of Appointment" (PDF). TU Munich. Retrieved 12 April 2016.


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=715027630"