Lawrence Paulson

Short description: American computer scientist

Lawrence Paulson

FRS

Error creating thumbnail: Unable to save thumbnail to destination

Lawrence Paulson at the Royal Society admissions day in London, July 2017

Born|

Lawrence Charles Paulson

1955 (age 70-71)[1]
Citizenship| US/UK
Alma mater|

* California Institute of Technology (BSc)
* Stanford University (PhD)

Known for|

* ML
* Isabelle[2]
* MetiTarski[3]

Spouse(s)|

* Susan Mary Paulson (d. 2010)
* Elena Tchougounova

Awards|

* ACM Fellow (2008)[4]

Scientific career
Fields|

* Theorem proving[5]
* Formal methods[5]
* Computer security[5]

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 FRS[2] (born 1955)[1] 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

* 1 Education
* 2 Research
* 3 Awards and honours
* 4 Personal life
* 5 References

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

## References

1. ↑ 1.0 1.1 1.2 Anon (2017). ",". Who's Who (online Oxford University Press ed.). A & C Black, an imprint of Bloomsbury Publishing plc. doi:10.1093/ww/9780199540884.013.289302. https://www.ukwhoswho.com/view/article/oupww/whoswho/U289302. (subscription or UK public library membership required)
2. ↑ 2.0 2.1 2.2 Anon (2017). "Professor Lawrence Paulson FRS". London: Royal Society. https://royalsociety.org/people/lawrence-paulson-13412/.
3. ↑ 3.0 3.1 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.
4. ↑ 4.0 4.1 Anon (2008). "Professor Lawrence C. Paulson". Association for Computing Machinery. http://awards.acm.org/award_winners/paulson_4585196.cfm.
5. ↑ 5.0 5.1 5.2 5.3 {{Google Scholar id}} template missing ID and not present in Wikidata.
6. ↑ 6.0 6.1 6.2 Lawrence Paulson at the Mathematics Genealogy Project
7. ↑ Lawrence Paulson author profile page at the ACM Digital Library
8. ↑ {{DBLP}} template missing ID and not present in Wikidata.
9. ↑ Lawrence Paulson publications indexed by the Scopus bibliographic database. (Subscription content?)
10. ↑ Lawrence Paulson Entry at ORCID
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. http://www.cl.cam.ac.uk/~lp15/MLbook/.
14. ↑ Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming 3 (3): 237–258. doi:10.1016/0743-1066(86)90015-4.
15. ↑ Paulson, Lawrence C. (1998). "The inductive approach to verifying cryptographic protocols". Journal of Computer Security 6 (1–2): 85–128. doi:10.3233/JCS-1998-61-205. ISSN 1875-8924.
16. ↑ Paulson, L. C. (2012). "Meti Tarski: Past and Future". Interactive Theorem Proving. Lecture Notes in Computer Science. 7406. pp. 1–10. doi:10.1007/978-3-642-32347-8_1. ISBN 978-3-642-32346-1.
17. ↑ Paulson, Larry. "Logic and Proof". University of Cambridge. http://www.cl.cam.ac.uk/teaching/1920/LogicProof/.
18. ↑ Paulson, Larry. "Foundations of Computer Science". http://www.cl.cam.ac.uk/teaching/1415/FoundsCS/.
19. ↑ "Department of Computer Science and Technology – Course pages 2017–18: Foundations of Computer Science". https://www.cl.cam.ac.uk/teaching/1718/FoundsCS/.
20. ↑ "Department of Computer Science and Technology – Course pages 2019–20: Foundations of Computer Science". https://www.cl.cam.ac.uk/teaching/1920/FoundsCS/.
21. ↑ "Certificate of Appointment". TU Munich. http://www4.in.tum.de/~paulson/Paulson-Certificate_of_appointment.pdf.
22. ↑ Paulson, Lawrence (2010). "Susan Paulson, PhD (1959–2010)". University of Cambridge. http://www.cl.cam.ac.uk/~lp15/Sue/.

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Lawrence Paulson. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Biography:Lawrence_Paulson&oldid=1071378"