АссистентНовый вопросИсторияОбласти знаний
Партнёрские проектыСпецпроектыСтать автором
Сменить язык
О РУВИКИ

Гордон, Майкл Дж. К.

Майкл Джон Ко́лдуэлл Го́рдон (англ. Michael John Caldwell Gordon; 28 февраля 1948[3], Рипон, Харрогейт, Норт-Йоркшир[d] — 22 августа 2017, Кембридж, Англия, Великобритания) — британский учёный в области информатики[4][5]. Известен как разработчик системы автоматического доказательства теорем HOL.

Общие сведения
Майкл Дж. К. Гордон
англ. Michael J. C. Gordon
Дата рождения 28 февраля 1948(1948-02-28)
Место рождения Рипон, Йоркшир, Англия
Дата смерти 22 августа 2017(2017-08-22) (69 лет)
Место смерти Кембридж, Англия
Страна
Образование
Род деятельности Информатика
Награды и премии

Биография

Майкл Гордон родился в Рипоне (Йоркшир, Англия). Учился в школах Дартингтон-Холл и Бидейлс. В 1966 году поступил в Колледж Гонвилл-энд-Киз для изучения инженерии, но перевёлся на математику. Летом 1969 года работал в Национальной физической лаборатории в Лондоне, где впервые познакомился с компьютерами.

Гордон получил степень доктора философии в Эдинбургском университете под руководством Рода Бёрстолла. В 1973 году защитил диссертацию на тему «Оценка и денотация чистых программ на LISP». Джон Маккарти пригласил его в Стэнфордский университет для работы в Лаборатории искусственного интеллекта. С 1981 года Гордон работал в Компьютерной лаборатории Кембриджского университета. В 1988 году стал лектором, а в 1996 году — профессором.

В 1994 году Гордон был избран членом Лондонского королевского общества[6]. В 2008 году в честь его 60-летия прошла двухдневная исследовательская встреча «Инструменты и методы верификации системной инфраструктуры»[7].

Был женат на Авре Кон, аспирантке Робина Милнера в Эдинбургском университете. Они проводили совместные исследования.

Гордон умер в Кембридже после непродолжительной болезни. У него остались жена и двое сыновей[4][8].

Карьера

Гордон руководил разработкой системы автоматического доказательства теорем HOL. Система HOL представляет собой среду для интерактивного доказательства теорем в логике высшего порядка. Её ключевой особенностью является высокая степень программируемости с помощью метаязыка ML. Система используется для формализации чистой математики и верификации промышленного оборудования.

По системе HOL проводится серия международных конференций TPHOLs[9]. Первые три конференции были неформальными встречами пользователей без публикации материалов. В настоящее время ежегодная конференция проводится на континенте, отличном от места проведения предыдущей встречи. С 1996 года тематика конференций расширилась и охватывает все аспекты доказательства теорем в логиках высшего порядка.

Примечания

  1. ↑ Bibliothèque nationale de France Autorités BnF (фр.): платформа открытых данных — 2011.
  2. ↑ Гордон, Майкл Дж. К. (англ.) в проекте «Математическая генеалогия»
  3. ↑ Michael J. C. Gordon // SNAC (англ.) — 2010.
  4. ↑ 1 2 Michael JC Gordon FRS, Professor Emeritus of Computer Assisted Reasoning, 28 February 1948 – 22 August 2017. Obituaries. UK: Computer Laboratory, University of Cambridge (2017). Дата обращения: 18 июня 2026.
  5. ↑ University of Cambridge Computer Laboratory. Michael JC Gordon FRS, Professor of Computer Assisted Reasoning (28 February 1948 – 22 August 2017) // Formal Aspects of Computing. — Springer International Publishing, 2017. — 27 октября (т. 29, № 6). — С. 933. — doi:10.1007/s00165-017-0438-y.
  6. ↑ Paulson, Lawrence C (2018). "Michael John Caldwell Gordon. 28 February 1948 – 22 August 2017". Biographical Memoirs of Fellows of the Royal Society. doi.org/10.1098/rsbm.2018.0019.
  7. ↑ Tools and Techniques for Verification of System Infrastructure. Дата обращения: 18 июня 2026.
  8. ↑ Kalvala, Sara Sad news regarding Mike Gordon. HOL theorem-proving system. SourceForge (22 августа 2017). Дата обращения: 18 июня 2026.
  9. ↑ TPHOLS, conferences associated with theorem proving in higher-order logics. UK: University of Cambridge. Дата обращения: 28 января 2014. Архивировано из оригинала 7 мая 2008 года.

Ссылки

Дополнительно по теме

Категории