stringtranslate.com

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

Лоуренс Чарльз Полсон FRS [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. ^ публикации abcd Лоуренса Полсона, проиндексированные Google Scholar
  3. ^ abc Лоуренс Полсон в проекте «Математическая генеалогия»
  4. ^ abc Анон (2017). «Полсон, профессор Лоуренс Чарльз» . Кто есть кто (онлайн- изд. Oxford University Press  ). Оксфорд: A&C Black. дои : 10.1093/ww/9780199540884.013.289302. (Требуется подписка или членство в публичной библиотеке Великобритании.)
  5. ^ abc Анон (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. ^ Лоуренс Полсон ORCID  0000-0003-0288-4279
  11. ^ Полсон, Лоуренс Чарльз (1981). Компилятор-генератор семантических грамматик (PDF) . cl.cam.ac.uk (кандидатская диссертация). Стэндфордский Университет. ОСЛК  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 г.


  • в
  • т
  • е