Lawrence Paulson  

Born  Lawrence Charles Paulson 1955 (age 65–66)^{[1]} 
Citizenship  US/UK 
Alma mater  
Known for  
Spouse(s) 

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 
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]}
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 compilercompilers 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 realvalued 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
 ^ ^{a} ^{b} ^{c} Anon (2017). "Paulson, Prof. Lawrence Charles". Who's Who. ukwhoswho.com (online Oxford University Press ed.). A & C Black, an imprint of Bloomsbury Publishing plc. doi:10.1093/ww/9780199540884.013.289302. (subscription or UK public library membership required) (subscription 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 RealValued Special Functions". Journal of Automated Reasoning. 44 (3): 175. CiteSeerX 10.1.1.157.3300. doi:10.1007/s1081700991492. S2CID 16215962.
 ^ ^{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
 ^ 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 0000000302884279
 ^ 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 9780521565431.
 ^ "ML for the Working Programmer". University of Cambridge. Retrieved 25 November 2015.
 ^ Paulson, L. C. (1986). "Natural deduction as higherorder resolution". The Journal of Logic Programming. 3 (3): 237–258. arXiv:cs/9301104. doi:10.1016/07431066(86)900154. S2CID 27085090.
 ^ Paulson, Lawrence C. (1998). "The inductive approach to verifying cryptographic protocols". Journal of Computer Security. 6 (1–2): 85–128. CiteSeerX 10.1.1.57.2049. doi:10.3233/JCS199861205. ISSN 18758924.
 ^ Paulson, L. C. (2012). "Meti Tarski: Past and Future". Interactive Theorem Proving. Lecture Notes in Computer Science. 7406. pp. 1–10. CiteSeerX 10.1.1.259.5577. doi:10.1007/9783642323478_1. ISBN 9783642323461.
 ^ 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.