Майкл Джей Си Гордон
Майкл Джей Си Гордон | |
|---|---|
 | |
| Рожденный | 28 февраля 1948 г. |
| Умер | 22 августа 2017 г. (69 лет) Кембридж , Англия |
| Альма-матер | Колледж Гонвилл и Кайус, Кембридж Эдинбургский университет |
| Известный | Средство доказательства теорем HOL |
| Научная карьера | |
| Поля | Информатика |
| Учреждения | Стэнфордский университет Кембриджский университет |
| Диссертация | Оценка и обозначение чистых программ LISP: проработанный пример семантики (1973) |
| Докторантура | Род Берстолл [1] |
Майкл Джон Колдуэлл Гордон, FRS (28 февраля 1948 — 22 августа 2017) — британский учёный-компьютерщик . [2] [3]
Жизнь
[ редактировать ]Майк Гордон родился в Рипоне , Йоркшир , Англия . [4] Он учился в школе Дартингтон-Холл и школе Бедейлс . В 1966 году его приняли на изучение инженерного дела в колледж Гонвилля и Кая , Кембриджского университета но перевели на математику . Во время учебы в 1969 году он работал в Национальной физической лаборатории в Лондоне летом , впервые познакомившись с компьютерами.
Гордон получил степень доктора философии в Эдинбургском университете под руководством Рода Берстолла , закончив в 1973 году диссертацией под названием «Оценка и обозначение программ на чистом LISP» . Он был приглашен в Стэнфордский университет в Калифорнии Джоном Маккарти , изобретателем LISP , для работы там в своей лаборатории искусственного интеллекта . Гордон работал в компьютерной лаборатории Кембриджского университета с 1981 года, сначала преподавателем, затем получил звание читателя в 1988 году и профессора в 1996 году.
он был избран членом Королевского общества . В 1994 году [5] двухдневная исследовательская встреча по инструментам и методам проверки системной инфраструктуры . а в 2008 году в честь его 60-летия там прошла [6]
Майк Гордон был женат на Авре Кон, аспирантке Робина Милнера в Эдинбургском университете , и они вместе проводили исследования. [4]
Он умер в Кембридже после непродолжительной болезни, у него остались жена и двое сыновей. [2] [7] [8]
Работа
[ редактировать ]Гордон руководил разработкой средства доказательства теорем HOL . Система HOL — это среда интерактивного доказательства теорем в логике высшего порядка . Его наиболее выдающейся особенностью является высокая степень программирования с помощью метаязыка ML . Система имеет широкий спектр применений: от формализации чистой математики до проверки промышленного оборудования.
Была проведена серия международных конференций по системе HOL, TPHOLs. [9] Первые три были неофициальными встречами пользователей без опубликованных протоколов. Теперь стало традицией проводить ежегодную конференцию на континенте, отличном от места проведения предыдущей встречи. С 1996 года сфера охвата расширилась и теперь охватывает все доказательства теорем в логике высшего порядка.
Ссылки
[ редактировать ]- ^ Майкл Дж. К. Гордон в проекте «Математическая генеалогия»
- ^ Jump up to: а б «Майкл Дж. К. Гордон, FRS, почетный профессор компьютерного рассуждения, 28 февраля 1948 г. - 22 августа 2017 г.» . Некрологи . Великобритания: Компьютерная лаборатория Кембриджского университета . 2017 . Проверено 2 сентября 2017 г.
- ^ Компьютерная лаборатория Кембриджского университета (27 октября 2017 г.). «Майкл Дж. К. Гордон, FRS, профессор компьютерного рассуждения (28 февраля 1948 г. - 22 августа 2017 г.)» . Формальные аспекты вычислений . 29 (6). Springer International Publishing : 933. doi : 10.1007/s00165-017-0438-y .
- ^ Jump up to: а б Полсон, Лоуренс К. (11 июня 2018 г.). «Майкл Джон Колдуэлл Гордон (FRS 1994), 28 февраля 1948 г. - 22 августа 2017 г.». arXiv : 1806.04002 . дои : 10.1098/rsbm.2018.0019 . S2CID 47017843 .
{{cite journal}}: Для цитирования журнала требуется|journal=( помощь ) - ^ Полсон, Лоуренс С. (2018). «Майкл Джон Колдуэлл Гордон. 28 февраля 1948 г. - 22 августа 2017 г.». Биографические мемуары членов Королевского общества . doi.org/10.1098/rsbm.2018.0019 .
- ^ «Инструменты и методы проверки системной инфраструктуры» . Проверено 14 января 2023 г.
- ^ Калвала, Сара (22 августа 2017 г.). «Печальные новости о Майке Гордоне» . Система доказательства теорем HOL . СоурсФордж . Проверено 2 сентября 2017 г.
- ^ Боуэн, Джонатан П. (июнь 2020 г.). «В память: дань уважения пяти коллегам по формальным методам» (PDF) . ФАКТЫ ФАКС . 2020 (1). БКС-FACS : 13–29. дои : 10.13140/RG.2.2.13481.62560 .
- ^ «ТФОЛС, конференции, связанные с доказательством теорем в логике высшего порядка» . Великобритания: Кембриджский университет . Архивировано из оригинала 7 мая 2008 года . Проверено 28 января 2014 г.
Внешние ссылки
[ редактировать ]
- 1948 рождений
- смертей в 2017 году
- Люди из Рипона
- Люди, получившие образование в школе Бедейлс
- Выпускники колледжа Гонвилл и Кайус в Кембридже
- Выпускники Эдинбургского университета
- английские ученые-компьютерщики
- Формальные методы люди
- Сотрудники компьютерной лаборатории Кембриджского университета
- Члены Королевского общества
- Ученые Национальной физической лаборатории (Великобритания)