Lawrence Paulson
{{short description|American computer scientist}}
{{EngvarB|date=July 2017}}
{{Use dmy dates|date=July 2017}}
{{Infobox scientist
|name = Lawrence Paulson
| birth_name = Lawrence Charles Paulson
| honorific_suffix = {{post-nominals|size=100%|FRS}}
|image = Lawrence Paulson Royal Society.jpg
|image_size =
|caption = Paulson in 2017
|birth_date = {{Birth year and age|1955}}{{Who's Who | author= Anon| title=Paulson, Prof. Lawrence Charles | id = U289302 | year = 2017 | edition = online Oxford University Press|location=Oxford|doi=10.1093/ww/9780199540884.013.289302}}
|birth_place =
|death_date =
|death_place =
|residence =
|citizenship = US/UK
|nationality =
|ethnicity =
|fields = {{Plainlist|
| thesis_title = A Compiler Generator for Semantic Grammars
| thesis_year = 1981
| thesis_url = https://www.proquest.com/docview/303229537
|workplaces = University of Cambridge
Technical University of Munich
|alma_mater = {{Plainlist|
|doctoral_advisor = John L. Hennessy
|academic_advisors =
|doctoral_students =
|notable_students =
|known_for = {{Plainlist|
- ML
- Isabelle{{Cite web|url=https://royalsociety.org/people/lawrence-paulson-13412/|title=Professor Lawrence Paulson FRS|website=royalsociety.org|access-date=5 May 2017|publisher=Royal Society|location=London|author=Anon|year=2017}}
- MetiTarski{{Cite journal | doi = 10.1007/s10817-009-9149-2| title = Meti Tarski: An Automatic Theorem Prover for Real-Valued Special Functions| journal = Journal of Automated Reasoning| volume = 44| issue = 3| pages = 175| year = 2009| last1 = Akbarpour | first1 = B. | last2 = Paulson | first2 = L. C. | citeseerx = 10.1.1.157.3300| s2cid = 16215962}}}}
|influences =
|influenced =
| spouse = {{Plainlist|
- Susan Mary Paulson (d. 2010)
- Elena Tchougounova}}
|awards ={{Plainlist|
- ACM Fellow (2008)}}
|signature =
|footnotes =
| website = {{Official website}}
}}
Lawrence Charles Paulson 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.{{Google scholar id }}{{MathGenealogy|id= 25162}}{{ACMPortal|id=81100146628}}{{DBLP|name=Lawrence C. Paulson}}{{Scopus id}}
Education
Paulson graduated from the California Institute of Technology in 1977,Lawrence Paulson {{ORCID|0000-0003-0288-4279}} 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.{{cite thesis |degree=PhD |first=Lawrence Charles|last=Paulson |title=A Compiler Generator for Semantic Grammars |website=cl.cam.ac.uk|year=1981 |url=http://www.cl.cam.ac.uk/~lp15/papers/Reports/thesis.pdf|author-link=Lawrence Paulson|oclc=757240716|publisher=Stanford University}}
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.{{cite book | last = Paulson | first = Lawrence | title = ML for the working programmer | publisher = Cambridge University Press | location = Cambridge New York | year = 1996 | isbn = 978-0521565431 }}{{cite web|title=ML for the Working Programmer|url=http://www.cl.cam.ac.uk/~lp15/MLbook/|publisher=University of Cambridge|access-date=25 November 2015}} His research is based around the interactive theorem prover Isabelle, which he introduced in 1986.{{Cite journal | doi = 10.1016/0743-1066(86)90015-4| title = Natural deduction as higher-order resolution| journal = The Journal of Logic Programming| volume = 3| issue = 3| pages = 237–258| year = 1986| last1 = Paulson | first1 = L. C. | arxiv = cs/9301104| s2cid = 27085090}} He has worked on the verification of cryptographic protocols using inductive definitions,{{cite journal|last1=Paulson|first1=Lawrence C.|title=The inductive approach to verifying cryptographic protocols|journal=Journal of Computer Security|volume=6|issue=1–2|year=1998|pages=85–128|issn=1875-8924|doi=10.3233/JCS-1998-61-205 | arxiv=2105.06319|citeseerx=10.1.1.57.2049|s2cid=7591720 }} and he has also formalised the constructible universe of Kurt Gödel. Recently he has built a new theorem prover, MetiTarski, for real-valued special functions.{{Cite book | doi = 10.1007/978-3-642-32347-8_1| chapter = Meti Tarski: Past and Future| title = Interactive Theorem Proving| volume = 7406| pages = 1–10| series = Lecture Notes in Computer Science| year = 2012| last1 = Paulson | first1 = L. C. | isbn = 978-3-642-32346-1| citeseerx = 10.1.1.259.5577}}
Paulson taught an undergraduate lecture course in the Computer Science Tripos, entitled Logic and Proof{{cite web|url=http://www.cl.cam.ac.uk/teaching/1920/LogicProof/|title=Logic and Proof|last1=Paulson|first1=Larry|publisher=University of Cambridge|access-date=27 January 2020}} which covers automated theorem proving and related methods. He also used to teach Foundations of Computer Science{{cite web|url=http://www.cl.cam.ac.uk/teaching/1415/FoundsCS/|title=Foundations of Computer Science|last1=Paulson|first1=Larry|access-date=25 November 2015}} which introduces functional programming, but this course was taken over by Alan Mycroft and Amanda Prorok in 2017,{{Cite web|url=https://www.cl.cam.ac.uk/teaching/1718/FoundsCS/|title=Department of Computer Science and Technology – Course pages 2017–18: Foundations of Computer Science|website=www.cl.cam.ac.uk|access-date=2020-01-27}} and then Anil Madhavapeddy and Amanda Prorok in 2019.{{Cite web|url=https://www.cl.cam.ac.uk/teaching/1920/FoundsCS/|title=Department of Computer Science and Technology – Course pages 2019–20: Foundations of Computer Science|website=www.cl.cam.ac.uk|access-date=2020-01-27}}
Awards and honours
Paulson was elected a Fellow of the Royal Society (FRS) in 2017, a Fellow of the Association for Computing Machinery in 2008{{cite web|title=Professor Lawrence C. Paulson|url=http://awards.acm.org/award_winners/paulson_4585196.cfm|website=awards.acm.org|author=Anon|year=2008|publisher=Association for Computing Machinery|access-date=12 April 2016}} and a Distinguished Affiliated Professor for Logic in Informatics at the Technical University of Munich.{{when|date=December 2017}}{{cite web|title=Certificate of Appointment|url=http://www4.in.tum.de/~paulson/Paulson-Certificate_of_appointment.pdf|publisher=TU Munich|access-date=12 April 2016}}
Personal life
Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010.{{cite web|title=Susan Paulson, PhD (1959–2010)|url=http://www.cl.cam.ac.uk/~lp15/Sue/|access-date=25 November 2015|first=Lawrence|last=Paulson|year=2010|publisher=University of Cambridge}} Since 2012, he has been married to Dr Elena Tchougounova.
References
{{reflist}}
{{FRS 2017}}
{{Authority control}}
{{DEFAULTSORT:Paulson, Lawrence}}
Category:American computer scientists
Category:Members of the University of Cambridge Computer Laboratory
Category:California Institute of Technology alumni
Category:Stanford University alumni
Category:Fellows of Clare College, Cambridge
Category:2008 fellows of the Association for Computing Machinery
Category:Fellows of the Royal Society
Category:Formal methods people
{{compu-bio-stub}}