Lawrence'a Paulsona

Lawrence'a Paulsona FRS
Lawrence Paulson w dniu przyjęć do Towarzystwa Królewskiego w Londynie, lipiec 2017 r
Urodzić się	Lawrence’a Charlesa Paulsona 1955 (wiek 67–68 lat)
Obywatelstwo	Stany Zjednoczone/Wielka Brytania
Alma Mater	Kalifornijski Instytut Technologiczny (licencjat) Uniwersytet Stanforda (doktorat)
Znany z	ML Izabela MetiTarski
Małżonkowie	Susan Mary Paulson (zm. 2010) Jelena Czougounowa
Nagrody	Stypendysta ACM (2008)
Kariera naukowa
Pola	Dowód twierdzenia Metody formalne Bezpieczeństwo komputera
Instytucje	University of Cambridge Uniwersytet Techniczny w Monachium
Praca dyplomowa	Generator kompilatorów dla gramatyk semantycznych (1981)
Doradca doktorski	Johna L. Hennessy'ego
Strona internetowa	www .cl .cam .ac .uk /~lp15 /

Lawrence Charles Paulson FRS (ur. 1955) to amerykański informatyk . Jest profesorem logiki obliczeniowej na University of Cambridge Computer Laboratory i członkiem Clare College w Cambridge .

Edukacja

Paulson ukończył California Institute of Technology w 1977 r., a tytuł doktora informatyki uzyskał na Uniwersytecie Stanforda w 1981 r. za badania nad językami programowania i kompilatorami-kompilatorami pod kierunkiem Johna L. Hennessy'ego .

Badania

Paulson przybył na Uniwersytet Cambridge w 1983 roku i został członkiem Clare College w Cambridge w 1987 roku. Najbardziej znany jest z tekstu o kamieniu węgielnym dotyczącym języka programowania ML , ML for the Working Programmer . Jego badania opierają się na interaktywnym dowodzie twierdzeń Isabelle , który wprowadził w 1986 roku. Pracował nad weryfikacją protokołów kryptograficznych za pomocą definicji indukcyjnych , a także sformalizował konstruowalny wszechświat Kurta Gödla . Niedawno zbudował nowy dowód twierdzeń, MetiTarski, dla funkcji specjalnych o wartościach rzeczywistych.

Paulson prowadzi kurs wykładów licencjackich w Computer Science Tripos , zatytułowany Logika i dowód , który obejmuje zautomatyzowane dowodzenie twierdzeń i powiązane metody. (Kiedyś uczył podstaw informatyki , które wprowadzają programowanie funkcyjne , ale ten kurs przejęli Alan Mycroft i Amanda Prorok w 2017 r., a następnie Anil Madhavapeddy i Amanda Prorok w 2019 r.)

Nagrody i wyróżnienia

Paulson został wybrany członkiem Towarzystwa Królewskiego (FRS) w 2017 r. , członkiem Stowarzyszenia Maszyn Komputerowych w 2008 r. oraz wybitnym profesorem stowarzyszonym logiki w informatyce na Uniwersytecie Technicznym w Monachium .

Życie osobiste

Paulson ma dwoje dzieci ze swoją pierwszą żoną, dr Susan Mary Paulson, która zmarła w 2010 roku. Od 2012 roku jest żonaty z dr Eleną Tchougounovą.