Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

Майкл Дж. К. Гордон
ProfessorMichaelJCGordon.jpg
Родившийся( 1948-02-28 )28 февраля 1948 г.
Рипон , Йоркшир , Англия
Умер22 августа 2017 г. (2017-08-22)(69 лет)
Кембридж , Англия
НациональностьБританский
Гражданствообъединенное Королевство
Альма-матерКолледж Гонвилля и Кая, Кембриджский
университет Эдинбурга
ИзвестенИнструмент доказательства теорем HOL
Научная карьера
ПоляИнформатика
УчрежденияСтэнфордский университет
Кембриджский университет
ТезисОценка и обозначение чистых программ LISP: рабочий пример в семантике  (1973)
ДокторантРод Берстолл [1]

Майкл Джон Колдуэлл Гордон FRS (28 февраля 1948 - 22 августа 2017) был ведущим британским ученым-компьютерщиком . [2] [3]

Жизнь [ править ]

Майк Гордон родился в Рипоне , Йоркшир , Англия . [4] Он учился в школе Дартингтон Холл и школе Бедейлз . В 1966 году он был принят на учебу инженерию в Gonville и Киз Колледж , Кембриджский университет , но переданы в математике . Во время учебы в 1969 году он летом работал в Национальной физической лаборатории в Лондоне , впервые познакомившись с компьютерами.

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

Он был избран членом Королевского общества в 1994 году [5], а в 2008 году в честь его 60-летия здесь была проведена двухдневная исследовательская встреча по инструментам и методам проверки системной инфраструктуры . [6]

Майк Гордон был женат на Avra Кона , кандидатской студент Робин Милнер в Эдинбургском университете , и они проводили исследования вместе. [4]

Он умер в Кембридже после непродолжительной болезни, у него остались жена и двое сыновей. [2] [7] [8]

Работа [ править ]

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

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

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

  1. ↑ Майкл Дж. К. Гордон в проекте « Математическая генеалогия»
  2. ^ a b «Майкл Дж. К. Гордон, FRS, заслуженный профессор компьютерного мышления, 28 февраля 1948 - 22 августа 2017» . Некрологи . Великобритания: Компьютерная лаборатория Кембриджского университета . 2017 . Проверено 2 сентября 2017 года .
  3. ^ Компьютерная лаборатория Кембриджского университета (27 октября 2017 г.). «Майкл Дж. К. Гордон FRS, профессор компьютерного мышления (28 февраля 1948 - 22 августа 2017)» . Формальные аспекты вычислений . Издательство Springer International . 29 (6): 933. DOI : 10.1007 / s00165-017-0438-у .
  4. ^ a b Полсон, Лоуренс К. (11 июня 2018 г.). «Майкл Джон Колдуэлл Гордон (ФРС 1994), 28 февраля 1948 - 22 августа 2017». arXiv : 1806.04002 . DOI : 10,1098 / rsbm.2018.0019 . S2CID 47017843 .  Цитировать журнал требует |journal=( помощь )
  5. ^ Полсон, Лоуренс C (2018). «Майкл Джон Колдуэлл Гордон. 28 февраля 1948 г. - 22 августа 2017 г.». Биографические воспоминания членов Королевского общества . doi.org/10.1098/rsbm.2018.0019 .
  6. ^ «Инструменты и методы для проверки системной инфраструктуры» . Проверено 28 января 2014 .
  7. ^ Kalvala, Sara (22 августа 2017). «Печальные новости о Майке Гордоне» . Система доказательства теорем HOL . SourceForge . Проверено 2 сентября 2017 года .
  8. ^ Боуэн, Джонатан П. (июнь 2020 г.). «In Memoriam: дань уважения пяти коллегам по формальным методам» (PDF) . FACS ФАКТЫ . BCS-FACS . 2020 (1): 13–29. DOI : 10,13140 / RG.2.2.13481.62560 .
  9. ^ "TPHOLS, конференции, связанные с доказательством теорем в логике высшего порядка" . Великобритания: Кембриджский университет . Архивировано из оригинала 7 мая 2008 года . Проверено 28 января 2014 .

Внешние ссылки [ править ]

  • Домашняя страница Майка Гордона