Робин Полсон: Американский учёный в области компьютерных наук
Lawrence Paulson
Российский ученый-информатик, профессор Кембриджского университета. Автор книги ML for the Working Programmer. Исследования в области языков программирования.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Американский учёный-компьютерщик (род. 1955) — американский учёный-компьютерщик. Он является профессором вычислительной логики в компьютерной лаборатории Кембриджского университета и членом Клэр-колледжа (Clare College) в Кембридже.
ACM Fellow (2008) (born 1955) is an American computer scientist. He is a Professor of Computational Logic at the University of Cambridge Computer Laboratory and a Fellow of Clare College, Cambridge.
Образование
Полсон окончил Калифорнийский технологический институт в 1977 году и получил степень доктора философии в области компьютерных наук в Стэнфордском университете в 1981 году за исследования в области языков программирования и генераторов компиляторов под руководством Джона Л. Хеннесси.
Paulson graduated from the California Institute of Technology in 1977, and obtained his PhD in Computer Science from Stanford University in 1981 for research on programming languages and compiler compilers supervised by John L. Hennessy.
Исследования
Полсон поступил в Кембриджский университет в 1983 году и в 1987 году стал членом Клэр-колледжа, Кембридж. Он наиболее известен своим основополагающим трудом по языку программирования ML – "ML for the Working Programmer". Его исследования базируются на интерактивной системе доказательства теорем Isabelle, которую он представил в 1986 году. Он занимался верификацией криптографических протоколов с использованием индуктивных определений, а также формализовал конструктивную вселенную Курта Гёделя. В последнее время он разработал новую систему доказательства теорем MetiTarski.
Paulson came to the University of Cambridge in 1983 and became a Fellow of Clare College, Cambridge in 1987. He is best known for the cornerstone text on the programming language ML, ML for the Working Programmer. His research is based around the interactive theorem prover Isabelle, which he introduced in 1986. He has worked on the verification of cryptographic protocols using inductive definitions, and he has also formalised the constructible universe of Kurt Gödel. Recently he has built a new theorem prover, MetiTarski,
Полсон читает вводный курс лекций по компьютерным наукам в рамках программы Tripos под названием "Логика и доказательства", охватывающий автоматическое доказательство теорем и смежные методы. (Ранее он преподавал курс "Основы компьютерных наук", вводящий в функциональное программирование, но в 2017 году этот курс перешел к Алану Майкрофту и Аманде Пророк, а в 2019 году – к Анилу Мадхавапедди и Аманде Пророк.)
Paulson teaches an undergraduate lecture course in the Computer Science Tripos, entitled Logic and Proof which covers automated theorem proving and related methods. (He used to teach Foundations of Computer Science which introduces functional programming, but this course was taken over by Alan Mycroft and Amanda Prorok in 2017, and then Anil Madhavapeddy and Amanda Prorok in 2019.)
Награды и почести
В 2017 году Полсон был избран членом (Fellow) Королевского общества (FRS) и назначен выдающимся приглашенным профессором логики в информатике в Техническом университете Мюнхена.
Paulson was elected a Fellow of the Royal Society (FRS) in 2017, and a Distinguished Affiliated Professor for Logic in Informatics at the Technical University of Munich.
Личная жизнь
У Полсона двое детей от его первой жены, доктора Сьюзан Мэри Полсон, скончавшейся в 2010 году. С 2012 года он женат на докторе Елене Чугуновой.
Paulson has two children by his first wife, Dr Susan Mary Paulson, who died in 2010. Since 2012, he has been married to Dr Elena Tchougounova.