Лоуренс Полсон

Лоуренс Полсон
ФРС
Лоуренс Полсон ФРС
	Лоуренс Полсон на в Королевское общество в Лондоне, июль 2017 г. приеме
Рожденный	Лоуренс Чарльз Полсон ; 1955 (68–69 лет)
Гражданство	США/Великобритания
Альма-матер	Калифорнийский технологический институт (бакалавр) ; Стэнфордский университет (доктор философии) ;
Известный	МЛ ; Изабель ; Положите Тарского ;
Супруги	Сьюзан Мэри Полсон (ум. 2010 г.) ; Елена Чугунова ;
Награды	Сотрудник ACM (2008 г.) ;
	Научная карьера
Поля	Доказательство теоремы ; Формальные методы ; Компьютерная безопасность ;
Учреждения	Кембриджский университет ; Технический университет Мюнхена
Диссертация	Компилятор-генератор семантических грамматик (1981)
Докторантура	Джон Л. Хеннесси
Веб-сайт	www .cl .камера .и .uk /~lp15 /

Лоуренс Чарльз Полсон, ФРС ^[5] (1955 г.р.) ^[4] — американский учёный-компьютерщик . Он является профессором вычислительной логики в компьютерной лаборатории Кембриджского университета и членом Клэр -колледжа в Кембридже . ^[2]^[3]^[7]^[8]^[9]

Образование

Полсон окончил Калифорнийский технологический институт в 1977 году. ^[10] и получил докторскую степень в области компьютерных наук в Стэнфордском университете в 1981 году за исследования языков программирования и компиляторов-компиляторов под руководством Джона Л. Хеннесси . ^[3]^[11]

Исследовать

Полсон поступил в Кембриджский университет в 1983 году и стал членом Клэр-колледжа в Кембридже в 1987 году. Он наиболее известен благодаря основополагающему тексту по языку программирования ML , ML для работающего программиста . ^[12]^[13] Его исследования основаны на интерактивном средстве доказательства теорем Isabelle , которое он представил в 1986 году. ^[14] Он работал над проверкой криптографических протоколов с использованием индуктивных определений . ^[15] и он также формализовал конструктивную вселенную Курта Гёделя . Недавно он построил новый прибор для доказательства теорем MetiTarski. ^[6] для вещественных специальных функций. ^[16]

Полсон читает курс лекций для студентов в рамках Computer Science Tripos под названием «Логика и доказательство» . ^[17] который охватывает автоматическое доказательство теорем и связанные с ним методы. (Раньше он преподавал основы информатики ^[18] который знакомит с функциональным программированием , но этот курс взяли на себя Алан Майкрофт и Аманда Пророк в 2017 году, ^[19] а затем Анил Мадхавапедди и Аманда Пророк в 2019 году. ^[20])

Награды и почести

Полсон был избран членом Королевского общества (FRS) в 2017 году . ^[5] член Ассоциации вычислительной техники в 2008 г. ^[1] и заслуженный профессор логики в информатике Мюнхенского технического университета . ^{[ когда? ]}^[21]

Личная жизнь

У Полсона двое детей от первой жены, доктора Сьюзен Мэри Полсон, которая умерла в 2010 году. ^[22] С 2012 года женат на докторе Елене Чугуновой. ^[4]

Ссылки

^ Jump up to: ^а ^б Анон (2008). «Профессор Лоуренс К. Полсон» . Награды.acm.org . Ассоциация вычислительной техники . Проверено 12 апреля 2016 г.
^ Jump up to: ^а ^б ^с ^д Публикации Лоуренса Полсона , проиндексированные Google Scholar
^ Jump up to: ^а ^б ^с Лоуренс Полсон в проекте «Математическая генеалогия»
^ Jump up to: ^а ^б ^с Анон (2017). «Полсон, профессор Лоуренс Чарльз» . Кто есть кто (онлайн- изд. Oxford University Press ). Оксфорд: A&C Black. дои : 10.1093/ww/9780199540884.013.289302 . (Требуется подписка или членство в публичной библиотеке Великобритании .)
^ Jump up to: ^а ^б ^с Анон (2017). «Профессор Лоуренс Полсон, ФРС» . royalsociety.org . Лондон: Королевское общество . Проверено 5 мая 2017 г.
^ Jump up to: ^а ^б Акбарпур, Б.; Полсон, LC (2009). «Мети Тарский : автоматическое средство доказательства теорем для специальных функций с действительным знаком». Журнал автоматизированного рассуждения . 44 (3): 175. CiteSeerX 10.1.1.157.3300 . дои : 10.1007/s10817-009-9149-2 . S2CID 16215962 .
^ Лоуренса Полсона Страница профиля автора ACM. в цифровой библиотеке
^ Лоуренс К. Полсон на DBLP библиографическом сервере
^ Публикации Лоуренса Полсона , индексируемые библиографической базой данных Scopus . (требуется подписка)
^ Лоуренс Полсон ОРЦИД 0000-0003-0288-4279
^ Полсон, Лоуренс Чарльз (1981). Компилятор-генератор семантических грамматик (PDF) . cl.cam.ac.uk (кандидатская диссертация). Стэнфордский университет. OCLC 757240716 .
^ Полсон, Лоуренс (1996). ML для работающего программиста . Кембридж, Нью-Йорк: Издательство Кембриджского университета. ISBN 978-0521565431 .
^ «ML для работающего программиста» . Кембриджский университет . Проверено 25 ноября 2015 г.
^ Полсон, LC (1986). «Естественная дедукция как разрешение высшего порядка». Журнал логического программирования . 3 (3): 237–258. arXiv : cs/9301104 . дои : 10.1016/0743-1066(86)90015-4 . S2CID 27085090 .
^ Полсон, Лоуренс К. (1998). «Индуктивный подход к проверке криптографических протоколов». Журнал компьютерной безопасности . 6 (1–2): 85–128. arXiv : 2105.06319 . CiteSeerX 10.1.1.57.2049 . дои : 10.3233/JCS-1998-61-205 . ISSN 1875-8924 . S2CID 7591720 .
^ Полсон, LC (2012). «Мети Тарский : прошлое и будущее». Интерактивное доказательство теорем . Конспекты лекций по информатике . Том. 7406. стр. 1–10. CiteSeerX 10.1.1.259.5577 . дои : 10.1007/978-3-642-32347-8_1 . ISBN 978-3-642-32346-1 .
^ Полсон, Ларри. «Логика и доказательство» . Кембриджский университет . Проверено 27 января 2020 г.
^ Полсон, Ларри. «Основы информатики» . Проверено 25 ноября 2015 г.
^ «Кафедра компьютерных наук и технологий - Страницы курса 2017–18: Основы информатики» . www.cl.cam.ac.uk. Проверено 27 января 2020 г.
^ «Кафедра компьютерных наук и технологий - Страницы курса 2019–20: Основы информатики» . www.cl.cam.ac.uk. Проверено 27 января 2020 г.
^ «Свидетельство о назначении» (PDF) . ТУ Мюнхен . Проверено 12 апреля 2016 г.
^ Полсон, Лоуренс (2010). «Сьюзен Полсон, доктор философии (1959–2010)» . Кембриджский университет . Проверено 25 ноября 2015 г.

Эта биографическая статья о компьютерном специалисте незавершена . Вы можете помочь Википедии, расширив ее .

[facm-1] Jump up to: ^а ^б Анон (2008). «Профессор Лоуренс К. Полсон» . Награды.acm.org . Ассоциация вычислительной техники . Проверено 12 апреля 2016 г.

[googlescholar-2] Jump up to: ^а ^б ^с ^д Публикации Лоуренса Полсона , проиндексированные Google Scholar

[mathgene-3] Jump up to: ^а ^б ^с Лоуренс Полсон в проекте «Математическая генеалогия»

[whoswho-4] Jump up to: ^а ^б ^с Анон (2017). «Полсон, профессор Лоуренс Чарльз» . Кто есть кто (онлайн- изд. Oxford University Press ). Оксфорд: A&C Black. дои : 10.1093/ww/9780199540884.013.289302 . (Требуется подписка или членство в публичной библиотеке Великобритании .)

[frs-5] Jump up to: ^а ^б ^с Анон (2017). «Профессор Лоуренс Полсон, ФРС» . royalsociety.org . Лондон: Королевское общество . Проверено 5 мая 2017 г.

[metitarski-6] Jump up to: ^а ^б Акбарпур, Б.; Полсон, LC (2009). «Мети Тарский : автоматическое средство доказательства теорем для специальных функций с действительным знаком». Журнал автоматизированного рассуждения . 44 (3): 175. CiteSeerX 10.1.1.157.3300 . дои : 10.1007/s10817-009-9149-2 . S2CID 16215962 .

[acm-7] Лоуренса Полсона Страница профиля автора ACM. в цифровой библиотеке

[dblp-8] Лоуренс К. Полсон на DBLP библиографическом сервере

[scopus-9] Публикации Лоуренса Полсона , индексируемые библиографической базой данных Scopus . (требуется подписка)

[orcid-10] Лоуренс Полсон ОРЦИД 0000-0003-0288-4279

[phd-11] Полсон, Лоуренс Чарльз (1981). Компилятор-генератор семантических грамматик (PDF) . cl.cam.ac.uk (кандидатская диссертация). Стэнфордский университет. OCLC 757240716 .

[12] Полсон, Лоуренс (1996). ML для работающего программиста . Кембридж, Нью-Йорк: Издательство Кембриджского университета. ISBN 978-0521565431 .

[13] «ML для работающего программиста» . Кембриджский университет . Проверено 25 ноября 2015 г.

[14] Полсон, LC (1986). «Естественная дедукция как разрешение высшего порядка». Журнал логического программирования . 3 (3): 237–258. arXiv : cs/9301104 . дои : 10.1016/0743-1066(86)90015-4 . S2CID 27085090 .

[Paulson1998-15] Полсон, Лоуренс К. (1998). «Индуктивный подход к проверке криптографических протоколов». Журнал компьютерной безопасности . 6 (1–2): 85–128. arXiv : 2105.06319 . CiteSeerX 10.1.1.57.2049 . дои : 10.3233/JCS-1998-61-205 . ISSN 1875-8924 . S2CID 7591720 .

[16] Полсон, LC (2012). «Мети Тарский : прошлое и будущее». Интерактивное доказательство теорем . Конспекты лекций по информатике . Том. 7406. стр. 1–10. CiteSeerX 10.1.1.259.5577 . дои : 10.1007/978-3-642-32347-8_1 . ISBN 978-3-642-32346-1 .

[17] Полсон, Ларри. «Логика и доказательство» . Кембриджский университет . Проверено 27 января 2020 г.

[18] Полсон, Ларри. «Основы информатики» . Проверено 25 ноября 2015 г.

[19] «Кафедра компьютерных наук и технологий - Страницы курса 2017–18: Основы информатики» . www.cl.cam.ac.uk. Проверено 27 января 2020 г.

[20] «Кафедра компьютерных наук и технологий - Страницы курса 2019–20: Основы информатики» . www.cl.cam.ac.uk. Проверено 27 января 2020 г.

[21] «Свидетельство о назначении» (PDF) . ТУ Мюнхен . Проверено 12 апреля 2016 г.

[22] Полсон, Лоуренс (2010). «Сьюзен Полсон, доктор философии (1959–2010)» . Кембриджский университет . Проверено 25 ноября 2015 г.

[4]

[5]

[6]

[1]

[2]

[3]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

v т и Члены Королевского общества, избранные в 2017 году.
Товарищи	Ив-Ален Бард Тони Белл Кристофер Бишоп Нил Берджесс Кейт Бевен Венди Бикмор Кришна Чаттерджи Джеймс Даррант Уоррен Ист Тим Эллиотт Энн Фергюсон-Смит Джонатан Грегори Марк Гросс Рой Харрисон Габриэле Хегерль Эдди Холмс Ричард Хоулстон Ивонн Джонс Subhash Khot Джулия Кинг Стаффорд Лайтман Ядвиндер Малхи Эндрю Маккензи Джерард Милберн Энн Невилл Элисон Ноубл Эндрю Орр-Юинг Дэвид Оуэн Лоуренс Полсон Жозефина Пембертон Санду Попеску Сара Прайс Энн Ридли Дэвид Рубинштейн Гэвин Салам Найджел Шедболт Ангус Сильвер Гордон Слэйд Пит Смит Никола Спалдин Джонатан Стой Джон Сазерленд Дж. Рой Тейлор Дженни Томас Патрик Валланс Сюзанна фон Кеммерер Хью Уоткинс Роджер Уильямс Кен Вульф Энди Вудс
Почетный	Дэвид Нойбергер
Иностранный	Макс Купер Уитфилд Диффи Роберт Граббс Хидео Хосоно Марсия МакНатт Гинес Мората Роберт Ричи Томас Зюдхоф Дэвид Тилман Сьюзан Весслер

Базы данных авторитетного контроля
Международный	ЯВЛЯЮТСЯ ВИАФ WorldCat
Национальный	Норвегия Франция Данные БнФ Израиль Соединенные Штаты Чешская Республика Нидерланды
академики	Ассоциация вычислительной техники ДБЛП Google Академика MathSciNet Проект математической генеалогии ОРЦИД Скопус zbMATH
Другой	ЗАКУСКА ИдРеф