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

Из Википедии, бесплатной энциклопедии

Лоуренс Полсон
Рожденный
Лоуренс Чарльз Полсон

1955 (68–69 лет) [4]
Гражданство США/Великобритания
Альма-матер
Известный
Супруги
  • Сьюзан Мэри Полсон (ум. 2010 г.)
  • Елена Чугунова
Награды
Научная карьера
Поля
Учреждения Кембриджский университет
Технический университет Мюнхена
Тезис Компилятор-генератор семантических грамматик   (1981)
Докторантура Джон Л. Хеннесси [3]
Веб-сайт www .cl .камера .Великобритания /~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]

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

  1. ^ Перейти обратно: а б Анон (2008). «Профессор Лоуренс К. Полсон» . Награды.acm.org . Ассоциация вычислительной техники . Проверено 12 апреля 2016 г.
  2. ^ Перейти обратно: а б с д Публикации Лоуренса Полсона, проиндексированные Google Scholar Отредактируйте это в Викиданных
  3. ^ Перейти обратно: а б с Лоуренс Полсон в проекте «Математическая генеалогия»
  4. ^ Перейти обратно: а б с Анон (2017). «Полсон, профессор Лоуренс Чарльз» . Кто есть кто (онлайн- изд. Oxford University Press ). Оксфорд: A&C Black. дои : 10.1093/ww/9780199540884.013.289302 . (Требуется подписка или членство в публичной библиотеке Великобритании .)
  5. ^ Перейти обратно: а б с Анон (2017). «Профессор Лоуренс Полсон, ФРС» . royalsociety.org . Лондон: Королевское общество . Проверено 5 мая 2017 г.
  6. ^ Перейти обратно: а б Акбарпур, Б.; Полсон, LC (2009). «Мети Тарский : автоматическое средство доказательства теорем для специальных функций с действительным знаком». Журнал автоматизированного рассуждения . 44 (3): 175. CiteSeerX   10.1.1.157.3300 . дои : 10.1007/s10817-009-9149-2 . S2CID   16215962 .
  7. ^ Лоуренса Полсона Страница профиля автора ACM. в цифровой библиотеке
  8. ^ Лоуренс К. Полсон на DBLP библиографическом сервере Отредактируйте это в Викиданных
  9. ^ Публикации Лоуренса Полсона, индексируемые библиографической базой данных Scopus . (требуется подписка)
  10. ^ Лоуренс Полсон ОРЦИД   0000-0003-0288-4279
  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 .
  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 г.