Майкл Джей Си Гордон

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

Майкл Джон Колдуэлл Гордон, 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 г.

Внешние ссылки

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

[1] Майкл Дж. К. Гордон в проекте «Математическая генеалогия»

[cl-obituary-2] Jump up to: ^а ^б «Майкл Дж. К. Гордон, FRS, почетный профессор компьютерного рассуждения, 28 февраля 1948 г. - 22 августа 2017 г.» . Некрологи . Великобритания: Компьютерная лаборатория Кембриджского университета . 2017 . Проверено 2 сентября 2017 г.

[fac-obituary-3] Компьютерная лаборатория Кембриджского университета (27 октября 2017 г.). «Майкл Дж. К. Гордон, FRS, профессор компьютерного рассуждения (28 февраля 1948 г. - 22 августа 2017 г.)» . Формальные аспекты вычислений . 29 (6). Springer International Publishing : 933. doi : 10.1007/s00165-017-0438-y .

[paulson18-4] Jump up to: ^а ^б Полсон, Лоуренс К. (11 июня 2018 г.). «Майкл Джон Колдуэлл Гордон (FRS 1994), 28 февраля 1948 г. - 22 августа 2017 г.». arXiv : 1806.04002 . дои : 10.1098/rsbm.2018.0019 . S2CID 47017843 . {{cite journal}}: Для цитирования журнала требуется |journal= ( помощь )

[5] Полсон, Лоуренс С. (2018). «Майкл Джон Колдуэлл Гордон. 28 февраля 1948 г. - 22 августа 2017 г.». Биографические мемуары членов Королевского общества . doi.org/10.1098/rsbm.2018.0019 .

[6] «Инструменты и методы проверки системной инфраструктуры» . Проверено 14 января 2023 г.

[hol-info-7] Калвала, Сара (22 августа 2017 г.). «Печальные новости о Майке Гордоне» . Система доказательства теорем HOL . СоурсФордж . Проверено 2 сентября 2017 г.

[bowen20-8] Боуэн, Джонатан П. (июнь 2020 г.). «В память: дань уважения пяти коллегам по формальным методам» (PDF) . ФАКТЫ ФАКС . 2020 (1). БКС-FACS : 13–29. дои : 10.13140/RG.2.2.13481.62560 .

[9] «ТФОЛС, конференции, связанные с доказательством теорем в логике высшего порядка» . Великобритания: Кембриджский университет . Архивировано из оригинала 7 мая 2008 года . Проверено 28 января 2014 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

Базы данных авторитетного контроля
International	ISNI VIAF WorldCat
National	France BnF data Germany Israel Belgium United States Netherlands Poland
Academics	DBLP MathSciNet Mathematics Genealogy Project Scopus zbMATH
People	Trove
Other	SNAC IdRef