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

Материал из Циклопедии
Перейти к навигации Перейти к поиску

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

англ. Michael J. C. Gordon
Файл:ProfessorMichaelJCGordon.jpg


Дата рождения
28 февраля 1948 года
Место рождения
Рипон, Йоркшир, Англия
Дата смерти
22 августа 2017 года
Место смерти
Кембридж, Англия


Род деятельности
Информатика
Место работы
Стэнфордский университет
Кембриджский университет





Майкл Джон Ко́лдуэлл Го́рдон (англ. Michael John Caldwell Gordon; [Нет даты!]) — британский учёный в области информатики[1][2]. Известен как разработчик системы автоматического доказательства теорем HOL.

Биография[править]

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

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

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

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

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

Карьера[править]

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

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

Примечания[править]

  1. ↑ 1,0 1,1 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.
  2. ↑ 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. — том 29. — № 6. — С. 933. — DOI:10.1007/s00165-017-0438-y
  3. ↑ 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.
  4. ↑ Tools and Techniques for Verification of System Infrastructure. Проверено 18 июня 2026.
  5. ↑ Kalvala, Sara Sad news regarding Mike Gordon. HOL theorem-proving system. SourceForge (22 August 2017). Проверено 18 июня 2026.
  6. ↑ TPHOLS, conferences associated with theorem proving in higher-order logics. UK: University of Cambridge. Архивировано из первоисточника 7 мая 2008.[недоступная ссылка] Проверено 28 января 2014.

Ссылки[править]

Рувики

Одним из источников, использованных при создании данной статьи, является статья из википроекта «Рувики» («ruwiki.ru») под названием «Гордон, Майкл Дж. К.», расположенная по адресу:

—https://ru.ruwiki.ru/wiki/Гордон,_Майкл_Дж._К.

Материал указанной статьи полностью или частично использован в Циклопедии по лицензии CC-BY-SA 4.0 и более поздних версий.

Всем участникам Рувики предлагается прочитать материал «Почему Циклопедия?».

Источник — http://cyclowiki.org/w/index.php?title=Гордон,_Майкл_Дж._К.&oldid=2679476