Lawrence Paulson
- California Institute of Technology (BSc)
- Stanford University (PhD)
- ML
- Isabelle[5]
- MetiTarski[6]
- Susan Mary Paulson (d. 2010)
- Elena Tchougounova
- ACM Fellow (2008)[1]
- Theorem proving[2]
- Formal methods[2]
- Computer security[2]
Technical University of Munich
Lawrence Charles Paulson FRS[5] (born 1955)[4] 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.[2][3][7][8][9]
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.[3][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,[6] 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,[5] a Fellow of the Association for Computing Machinery in 2008[1] 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.[4]
References
- ^ a b Anon (2008). "Professor Lawrence C. Paulson". awards.acm.org. Association for Computing Machinery. Retrieved 12 April 2016.
- ^ a b c d Lawrence Paulson publications indexed by Google Scholar
- ^ a b c Lawrence Paulson at the Mathematics Genealogy Project
- ^ a b c 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.)
- ^ a b c Anon (2017). "Professor Lawrence Paulson FRS". royalsociety.org. London: Royal Society. Retrieved 5 May 2017.
- ^ 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. CiteSeerX 10.1.1.157.3300. doi:10.1007/s10817-009-9149-2. S2CID 16215962.
- ^ Lawrence Paulson author profile page at the ACM Digital Library
- ^ Lawrence C. Paulson at DBLP Bibliography Server
- ^ Lawrence Paulson publications indexed by the Scopus bibliographic database. (subscription required)
- ^ Lawrence Paulson ORCID 0000-0003-0288-4279
- ^ Paulson, Lawrence Charles (1981). A Compiler Generator for Semantic Grammars (PDF). cl.cam.ac.uk (PhD thesis). Stanford University. OCLC 757240716.
- ^ Paulson, Lawrence (1996). ML for the working programmer. Cambridge New York: Cambridge University Press. ISBN 978-0521565431.
- ^ "ML for the Working Programmer". University of Cambridge. Retrieved 25 November 2015.
- ^ 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.
- ^ 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.
- ^ 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.
- ^ Paulson, Larry. "Logic and Proof". University of Cambridge. Retrieved 27 January 2020.
- ^ Paulson, Larry. "Foundations of Computer Science". Retrieved 25 November 2015.
- ^ "Department of Computer Science and Technology – Course pages 2017–18: Foundations of Computer Science". www.cl.cam.ac.uk. Retrieved 27 January 2020.
- ^ "Department of Computer Science and Technology – Course pages 2019–20: Foundations of Computer Science". www.cl.cam.ac.uk. Retrieved 27 January 2020.
- ^ "Certificate of Appointment" (PDF). TU Munich. Retrieved 12 April 2016.
- ^ Paulson, Lawrence (2010). "Susan Paulson, PhD (1959–2010)". University of Cambridge. Retrieved 25 November 2015.
- v
- t
- e
- Yves-Alain Barde
- Tony Bell
- Christopher Bishop
- Neil Burgess
- Keith Beven
- Wendy Bickmore
- Krishna Chatterjee
- James Durrant
- Warren East
- Tim Elliott
- Anne Ferguson-Smith
- Jonathan Gregory
- Mark Gross
- Roy Harrison
- Gabriele Hegerl
- Eddie Holmes
- Richard Houlston
- Yvonne Jones
- Subhash Khot
- Julia King
- Stafford Lightman
- Yadvinder Malhi
- Andrew McKenzie
- Gerard Milburn
- Anne Neville
- Alison Noble
- Andrew Orr-Ewing
- David Owen
- Lawrence Paulson
- Josephine Pemberton
- Sandu Popescu
- Sarah Price
- Anne Ridley
- David Rubinsztein
- Gavin Salam
- Nigel Shadbolt
- Angus Silver
- Gordon Slade
- Pete Smith
- Nicola Spaldin
- Jonathan Stoye
- John Sutherland
- J. Roy Taylor
- Jenny Thomas
- Patrick Vallance
- Susanne von Caemmerer
- Hugh Watkins
- Roger Williams
- Ken Wolfe
- Andy Woods
This biographical article relating to a computer specialist is a stub. You can help Wikipedia by expanding it. |
- v
- t
- e