Полсон, Лоуренс
Лоуренс Полсон
- Имя при рождении
- Лоуренс Чарльз Полсон
- Дата рождения
- 1955[1]
- Гражданство
- США / Великобритания
- Род деятельности
- учёный в области информатики
Лоуренс Чарльз Полсон ([Нет даты!]) — американский учёный в области информатики. Профессор вычислительной логики в Компьютерной лаборатории Кембриджского университета и член Клэр-колледжа в Кембридже[2][3]. Известен как автор базового учебника по языку программирования ML и создатель интерактивного средства доказательства теорем Isabelle.
Биография[править]
Полсон окончил Калифорнийский технологический институт в 1977 году[4]. В 1981 году получил степень доктора философии по информатике в Стэнфордском университете за исследования в области языков программирования и компиляторов компиляторов под руководством Джона Л. Хеннесси[2][5].
В 1983 году Полсон перешёл в Кембриджский университет. В 1987 году стал членом Клэр-колледжа. Он написал базовый учебник по языку программирования ML «ML for the Working Programmer»[6]. Его исследования связаны с интерактивным средством доказательства теорем Isabelle, которое он представил в 1986 году. Он работал над верификацией криптографических протоколов с использованием индуктивных определений, а также формализовал конструктивный универсум Курта Гёделя. Позднее он создал новое средство доказательства теорем MetiTarski для вещественнозначных специальных функций.
Полсон читал курс лекций для бакалавров «Логика и доказательство»[7], посвящённый автоматическому доказательству теорем и смежным методам. Он также преподавал курс «Основы информатики»[8], знакомящий с функциональным программированием. В 2017 году этот курс перешёл к Алану Майкрофту и Аманде Пророк[9], а в 2019 году — к Анилу Мадхавапедди и Аманде Пророк[10].
Личная жизнь[править]
У Полсона двое детей от первой жены, доктора Сьюзан Мэри Полсон, которая умерла в 2010 году[11]. С 2012 года он женат на докторе Елене Чугуновой[1].
Награды и звания[править]
В 2017 году Полсон был избран членом Лондонского королевского общества[12]. В 2008 году он стал членом Ассоциации вычислительной техники[13]. Также является почётным профессором логики в информатике Мюнхенского технического университета[14].
Примечания[править]
- ↑ 1,0 1,1 Paulson, Prof. Lawrence Charles. — Oxford, 2017. — DOI:10.1093/ww/9780199540884.013.289302
- ↑ 2,0 2,1 Полсон, Лоуренсангл. в проекте «Математическая генеалогия»
- ↑ Шаблон:Scopus id
- ↑ Lawrence Paulson
- ↑ Paulson, Lawrence Charles (1981), «A Compiler Generator for Semantic Grammars», Stanford University, OCLC 757240716, <http://www.cl.cam.ac.uk/~lp15/papers/Reports/thesis.pdf>. Проверено 24 июня 2026.
- ↑ ML for the Working Programmer. University of Cambridge. Проверено 24 июня 2026.
- ↑ Logic and Proof. University of Cambridge. Проверено 24 июня 2026.
- ↑ Foundations of Computer Science. Проверено 24 июня 2026.
- ↑ Department of Computer Science and Technology – Course pages 2017–18: Foundations of Computer Science. www.cl.cam.ac.uk. Проверено 24 июня 2026.
- ↑ Department of Computer Science and Technology – Course pages 2019–20: Foundations of Computer Science. www.cl.cam.ac.uk. Проверено 24 июня 2026.
- ↑ Paulson, Lawrence Susan Paulson, PhD (1959–2010). University of Cambridge (2010). Проверено 24 июня 2026.
- ↑ Anon Professor Lawrence Paulson FRS. London: Royal Society (2017). Проверено 24 июня 2026.
- ↑ Anon Professor Lawrence C. Paulson. Association for Computing Machinery (2008). Проверено 24 июня 2026.
- ↑ Certificate of Appointment. TU Munich. Проверено 24 июня 2026.
 | Одним из источников, использованных при создании данной статьи, является статья из википроекта «Рувики» («ruwiki.ru») под названием «Полсон, Лоуренс», расположенная по адресу:
Материал указанной статьи полностью или частично использован в Циклопедии по лицензии CC-BY-SA 4.0 и более поздних версий. Всем участникам Рувики предлагается прочитать материал «Почему Циклопедия?». |
|---|