Майкл Дж. К. Гордон - Michael J. C. Gordon
Майкл Дж. К. Гордон | |
|---|---|
 | |
| Родился |
28 февраля 1948 г. |
| Умер | 22 августа 2017 г. (69 лет)
Кембридж , Англия
|
| Национальность | Британский |
| Гражданство | Объединенное Королевство |
| Альма-матер |
Колледж Гонвилля и Кая, Кембриджский университет Эдинбурга |
| Известен | Инструмент доказательства теорем HOL |
| Научная карьера | |
| Поля | Информатика |
| Учреждения |
Стэнфордский университет Кембриджский университет |
| Тезис | Оценка и обозначение чистых программ LISP: рабочий пример в семантике (1973) |
| Докторант | Род Берстолл |
Майкл Джон Колдуэлл Гордон FRS (28 февраля 1948 - 22 августа 2017) был ведущим британским ученым-компьютерщиком .
Жизнь
Майк Гордон родился в Рипоне , Йоркшир , Англия . Он посещал Дартингтон Hall School и Bedales школу . В 1966 году он был принят на учебу инженерию в Gonville и Киз Колледж , Кембриджский университет , но переданы в математике . Во время учебы в 1969 году он летом работал в Национальной физической лаборатории в Лондоне , впервые познакомившись с компьютерами.
Гордон учился на докторскую степень в Эдинбургском университете под руководством Рода Берстолла и в 1973 году защитил диссертацию на тему « Оценка и обозначение чистых программ LISP» . Он был приглашен в Стэнфордский университет в Калифорнии по Джону Маккарти , изобретатель LISP , чтобы работать в его лаборатории искусственного интеллекта там. Гордон работал в компьютерной лаборатории Кембриджского университета с 1981 года, сначала в качестве преподавателя, затем стал читателем в 1988 году и профессором в 1996 году.
В 1994 году он был избран членом Королевского общества , а в 2008 году в честь его 60-летия здесь была проведена двухдневная исследовательская встреча по инструментам и методам проверки системной инфраструктуры .
Майк Гордон был женат на Avra Кона , кандидатской студент Робин Милнер в Эдинбургском университете , и они проводили исследования вместе.
Он умер в Кембридже после непродолжительной болезни, у него остались жена и двое сыновей.
Работа
Гордон руководил разработкой средства доказательства теорем HOL . Система HOL - это среда для интерактивного доказательства теорем в логике более высокого порядка . Его наиболее выдающейся особенностью является высокая степень программируемости с помощью метаязыка ML . Система имеет множество применений, от формализации чистой математики до проверки промышленного оборудования.
Был проведен ряд международных конференций по системе HOL, TPHOL. Первые три были неформальными встречами пользователей без опубликованных материалов. В настоящее время традиция заключается в проведении ежегодной конференции на континенте, отличном от места проведения предыдущей встречи. С 1996 года область применения расширилась, чтобы охватить все доказательства теорем в логике более высокого порядка.