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

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

В 1983 году Полсон перешёл в Кембриджский университет. В 1987 году стал членом Клэр-колледжа. Он написал базовый учебник по языку программирования ML «ML for the Working Programmer»^[7]. Его исследования связаны с интерактивным средством доказательства теорем Isabelle, которое он представил в 1986 году. Он работал над верификацией криптографических протоколов с использованием индуктивных определений, а также формализовал конструктивный универсум Курта Гёделя. Позднее он создал новое средство доказательства теорем MetiTarski для вещественнозначных специальных функций.

Полсон читал курс лекций для бакалавров «Логика и доказательство»^[8], посвящённый автоматическому доказательству теорем и смежным методам. Он также преподавал курс «Основы информатики»^[9], знакомящий с функциональным программированием. В 2017 году этот курс перешёл к Алану Майкрофту и Аманде Пророк^[10], а в 2019 году — к Анилу Мадхавапедди и Аманде Пророк^[11].

В 2017 году Полсон был избран членом Лондонского королевского общества^[13]. В 2008 году он стал членом Ассоциации вычислительной техники^[14]. Также является почётным профессором логики в информатике Мюнхенского технического университета^[15].