stringtranslate.com

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

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

Образование

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

Исследовать

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

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

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

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

Личная жизнь

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

Ссылки

  1. ^ ab Anon (2008). "Профессор Лоуренс К. Полсон". awards.acm.org . Ассоциация вычислительной техники . Получено 12 апреля 2016 г. .
  2. ^ abcd Публикации Лоуренса Полсона, проиндексированные Google Scholar
  3. ^ abc Лоуренс Полсон в проекте «Генеалогия математики»
  4. ^ ab Anon (2017). "Paulson, Prof. Lawrence Charles" . Who's Who (онлайн-редакция Oxford University Press  ). Oxford: A & C Black. doi : 10.1093/ww/9780199540884.013.289302. (Требуется подписка или членство в публичной библиотеке Великобритании.)
  5. ^ ab Anon (2017). "Профессор Лоуренс Полсон FRS". royalsociety.org . Лондон: Королевское общество . Получено 5 мая 2017 г.
  6. ^ ab Akbarpour, B.; Paulson, LC (2009). "Meti Tarski : Автоматический доказатель теорем для вещественнозначных специальных функций". Journal of Automated Reasoning . 44 (3): 175. CiteSeerX 10.1.1.157.3300 . doi :10.1007/s10817-009-9149-2. S2CID  16215962. 
  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 для работающего программиста . Кембридж, Нью-Йорк: Cambridge University Press. 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. arXiv : 2105.06319 . CiteSeerX 10.1.1.57.2049 . doi : 10.3233/JCS-1998-61-205. ISSN  1875-8924. S2CID  7591720. 
  16. ^ Paulson, LC (2012). "Meti Tarski : Past and Future". Интерактивное доказательство теорем . Lecture Notes in Computer Science . Vol. 7406. pp. 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–2020: Основы компьютерных наук". www.cl.cam.ac.uk . Получено 27 января 2020 г. .
  21. ^ "Свидетельство о назначении" (PDF) . TU Munich . Получено 12 апреля 2016 г. .
  22. ^ Полсон, Лоуренс (2010). "Сьюзан Полсон, доктор философии (1959–2010)". Кембриджский университет . Получено 25 ноября 2015 г.


  • в
  • т
  • е