Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Британский учёный в области компьютерных наук Майкл Джон Колдуэлл Гордон (28 февраля 1948 – 22 августа 2017) был британским учёным в области компьютерных наук.
British computer scientist
Michael John Caldwell Gordon (28 February 1948 – 22 August 2017) was a British computer scientist.
Жизнь
Майк Гордон родился в Рипоне, Йоркшир, Англия. Он учился в школе Дартингтон-Холл и школе Бедальс. В 1966 году его приняли на обучение по специальности «инженерия» в Гонвилл-энд-Кайус-колледж Кембриджского университета, но он перешел на математику. Во время учебы, летом 1969 года, он работал в Национальной физической лаборатории в Лондоне, где впервые познакомился с компьютерами. Гордон получил степень доктора философии в Эдинбургском университете под руководством Рода Бурстолла, защитив в 1973 году диссертацию под названием «Оценка и денотация чистых программ на LISP». Джон Маккарти, изобретатель LISP, пригласил его в Стэнфордский университет в Калифорнии для работы в своей лаборатории искусственного интеллекта. С 1981 года Гордон работал в компьютерной лаборатории Кембриджского университета, сначала в качестве лектора, затем в 1988 году был повышен до Reader, а в 1996 году – до профессора. В 1994 году он был избран членом Королевского общества, а в 2008 году в его честь была проведена двухдневная научно-исследовательская конференция, посвященная инструментам и методам верификации системной инфраструктуры, в связи с его 60-летием. Майк Гордон был женат на Авре Кон, аспирантке Робина Милнера в Эдинбургском университете, и они вместе занимались научными исследованиями.
Mike Gordon was born in Ripon, Yorkshire, England. He attended Dartington Hall School and Bedales School. In 1966, he was accepted to study engineering at Gonville and Caius College, University of Cambridge, but transferred to mathematics. During his studies, in 1969 he worked at the National Physical Laboratory in London during the summer, gaining his first exposure to computers. Gordon studied for his PhD degree at University of Edinburgh, supervised by Rod Burstall, finishing in 1973 with a thesis entitled Evaluation and Denotation of Pure LISP Programs. He was invited to Stanford University in California by John McCarthy, the inventor of LISP, to work in his Artificial Intelligence Laboratory there. Gordon worked at the Cambridge University Computer Laboratory from 1981, initially as a lecturer, promoted to Reader in 1988 and Professor in 1996. He was elected a Fellow of the Royal Society in 1994, and in 2008 a two day research meeting on Tools and Techniques for Verification of System Infrastructure was held there in honour of his 60th birthday. Mike Gordon was married to Avra Cohn, a PhD student of Robin Milner at the University of Edinburgh, and they undertook research together.
Работа
Гордон возглавил разработку системы доказательства теорем HOL. Система HOL – это среда для интерактивного доказательства теорем в логике высшего порядка. Её наиболее выдающейся особенностью является высокая степень программируемости посредством мета-языка ML. Система имеет широкий спектр применения, от формализации чистой математики до верификации промышленного оборудования. Проводилась серия международных конференций, посвященных системе HOL, – TPHOLs. Первые три были неформальными встречами пользователей без опубликованных материалов. В настоящее время существует традиция ежегодно проводить конференцию на континенте, отличном от места проведения предыдущей. Начиная с 1996 года, область охвата расширилась и включила в себя все доказательства теорем в логиках высшего порядка.
Gordon led the development of the HOL theorem prover. The HOL system is an environment for interactive theorem proving in a higher order logic. Its most outstanding feature is its high degree of programmability through the meta language ML. The system has a wide variety of uses, from formalising pure mathematics to verification of industrial hardware. There has been a series of international conferences on the HOL system, TPHOLs. The first three were informal users' meetings with no published proceedings. The tradition now is for an annual conference in a continent different from the location of the previous meeting. From 1996, the scope broadened to cover all theorem proving in higher order logics.