Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

ФРС
Королевское общество Лоуренса Полсона.jpg
Лоуренс Полсон на приеме в Королевское общество в Лондоне, июль 2017 г.
Родившийся
Лоуренс Чарльз Полсон

1955 (возраст 65–66 лет) [1]
ГражданствоСША / Великобритания
Альма-матер
Известен
Супруг (а)
  • Сьюзан Мэри Полсон (ум. 2010)
  • Елена Чугунова
Награды
Научная карьера
Поля
УчрежденияМюнхенский технический университет Кембриджского
университета
ТезисГенератор компилятора для семантических грамматик  (1981)
ДокторантДжон Л. Хеннесси [6]
Интернет сайтwww .cl .cam .ac .uk / ~ lp15 /

Лоуренс Чарльз Полсон FRS [2] (род. 1955) [1] - американский ученый-компьютерщик . Он является профессором в области вычислительной логики в Университете Кембриджа компьютерной лаборатории и научный сотрудник в Clare College, Кембридж . [5] [6] [7] [8] [9]

Образование [ править ]

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

Исследование [ править ]

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

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

Награды и награды [ править ]

Полсон был избран членом Королевского общества (FRS) в 2017 году , [2] член Ассоциации вычислительной техники в 2008 году [4] и Отличаясь Дочерним Профессор логики в информатике в Мюнхенском техническом университете . [ когда? ] [21]

Личная жизнь [ править ]

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

Ссылки [ править ]

  1. ^ а б в Анон (2017). "Полсон, профессор Лоуренс Чарльз" . Кто есть кто . ukwhoswho.com (онлайн- издательство Oxford University Press  ). A&C Black, отпечаток Bloomsbury Publishing plc. DOI : 10.1093 / WW / 9780199540884.013.289302 . ( требуется подписка или членство в публичной библиотеке Великобритании ) (требуется подписка)
  2. ^ а б в Анон (2017). "Профессор Лоуренс Полсон FRS" . royalsociety.org . Лондон: Королевское общество . Дата обращения 5 мая 2017 .
  3. ^ a b Akbarpour, B .; Полсон, LC (2009). «Мети Тарский : автоматическое средство доказательства теорем для вещественнозначных специальных функций». Журнал автоматизированных рассуждений . 44 (3): 175. CiteSeerX 10.1.1.157.3300 . DOI : 10.1007 / s10817-009-9149-2 . S2CID 16215962 .  
  4. ^ а б Анон (2008). "Профессор Лоуренс К. Полсон" . awards.acm.org . Ассоциация вычислительной техники . Проверено 12 апреля +2016 .
  5. ^ a b c d Публикации Лоуренса Полсона, проиндексированные Google Scholar
  6. ^ a b c Лоуренс Полсон в проекте « Математическая генеалогия»
  7. ^ Лоуренс Полсон страница профиля автора в ACM Digital Library
  8. ^ Лоуренс К. Полсон насервере библиографии DBLP
  9. ^ Лоуренс Полсон публикации индексированных Scopus библиографической базы данных. (требуется подписка)
  10. ^ Лоуренс Полсон ORCID 0000-0003-0288-4279 
  11. ^ Полсон, Лоуренс Чарльз (1981). Компилятор-генератор семантических грамматик (PDF) . cl.cam.ac.uk (кандидатская диссертация). Стэндфордский Университет. OCLC 757240716 .  
  12. ^ Полсон, Лоуренс (1996). ML для работающего программиста . Кембридж, Нью-Йорк: Издательство Кембриджского университета. ISBN 978-0521565431.
  13. ^ "ML для работающего программиста" . Кембриджский университет . Проверено 25 ноября 2015 года .
  14. Перейти ↑ Paulson, LC (1986). «Естественная дедукция как разрешение высшего порядка». Журнал логического программирования . 3 (3): 237–258. arXiv : cs / 9301104 . DOI : 10.1016 / 0743-1066 (86) 90015-4 . S2CID 27085090 . 
  15. ^ Полсон, Лоуренс С. (1998). «Индуктивный подход к верификации криптографических протоколов». Журнал компьютерной безопасности . 6 (1–2): 85–128. CiteSeerX 10.1.1.57.2049 . DOI : 10.3233 / JCS-1998-61-205 . ISSN 1875-8924 .  
  16. Перейти ↑ Paulson, LC (2012). «Мети Тарский : прошлое и будущее». Интерактивное доказательство теорем . Конспект лекций по информатике . 7406 . С. 1–10. CiteSeerX 10.1.1.259.5577 . DOI : 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 года .


  • v
  • т
  • е