Лоуренс Полсон - Lawrence Paulson

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

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

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

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

Образование

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

Исследование

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

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

Награды и награды

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

Личная жизнь

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

Рекомендации

  1. ^ а б c Анон (2017). "Полсон, профессор Лоуренс Чарльз". Кто есть кто. ukwhoswho.com (онлайн Oxford University Press ред.). A&C Black, отпечаток Bloomsbury Publishing plc. Дои:10.1093 / ww / 9780199540884.013.289302. (подписка или Членство в публичной библиотеке Великобритании требуется) (требуется подписка)
  2. ^ а б c Анон (2017). "Профессор Лоуренс Полсон FRS". royalsociety.org. Лондон: Королевское общество. Получено 5 мая 2017.
  3. ^ а б Akbarpour, B .; Полсон, Л. С. (2009). «Мети Тарский: Автоматическое средство доказательства теорем для вещественнозначных специальных функций ». Журнал автоматизированных рассуждений. 44 (3): 175. CiteSeerX  10.1.1.157.3300. Дои:10.1007 / s10817-009-9149-2. S2CID  16215962.
  4. ^ а б Анон (2008). "Профессор Лоуренс К. Полсон". awards.acm.org. Ассоциация вычислительной техники. Получено 12 апреля 2016.
  5. ^ а б c d Лоуренс Полсон публикации, проиндексированные Google ученый Отредактируйте это в Викиданных
  6. ^ а б c Лоуренс Полсон на Проект "Математическая генеалогия"
  7. ^ Лоуренс Полсон страница профиля автора на ACM Цифровая библиотека
  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. ^ Полсон, Л. К. (1986). «Естественная дедукция как разрешение высшего порядка». Журнал логического программирования. 3 (3): 237–258. arXiv:cs / 9301104. Дои:10.1016/0743-1066(86)90015-4. S2CID  27085090.
  15. ^ Полсон, Лоуренс К. (1998). «Индуктивный подход к верификации криптографических протоколов». Журнал компьютерной безопасности. 6 (1–2): 85–128. CiteSeerX  10.1.1.57.2049. Дои:10.3233 / JCS-1998-61-205. ISSN  1875-8924.
  16. ^ Полсон, Л. К. (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). TU Мюнхен. Получено 12 апреля 2016.
  22. ^ Полсон, Лоуренс (2010). «Сьюзан Полсон, доктор философии (1959–2010)». Кембриджский университет. Получено 25 ноября 2015.