Michaela JC Gordona

Michaela JC Gordona
Urodzić się	( 1948-02-28 ) 28 lutego 1948 Ripon , Yorkshire , Anglia
Zmarł	22 sierpnia 2017 (22.08.2017) (w wieku 69) Cambridge , Anglia
Alma Mater	Gonville and Caius College na Uniwersytecie Cambridge w Edynburgu
Znany z	Dowód twierdzenia HOL
Kariera naukowa
Pola	Informatyka
Instytucje	Uniwersytetu Stanforda w Cambridge
Praca dyplomowa	Ocena i oznaczenie czystych programów LISP: praktyczny przykład z semantyki (1973)
Doradca doktorski	Rod Burstall

Michael John Caldwell Gordon FRS (28 lutego 1948-22 sierpnia 2017) był brytyjskim informatykiem .

Życie

Mike Gordon urodził się w Ripon , Yorkshire , Anglia . Uczęszczał do Dartington Hall School i Bedales School . W 1966 roku został przyjęty na studia inżynierskie w Gonville and Caius College na Uniwersytecie w Cambridge , ale przeniósł się na matematykę . Podczas studiów, w 1969 roku , latem pracował w National Physical Laboratory w Londynie , gdzie po raz pierwszy zetknął się z komputerami.

Gordon studiował, aby uzyskać stopień doktora na Uniwersytecie w Edynburgu , pod kierunkiem Roda Burstall , kończąc w 1973 r. pracą zatytułowaną Ocena i oznaczenie programów czystego LISP-a . Został zaproszony na Uniwersytet Stanforda w Kalifornii przez Johna McCarthy'ego , wynalazcę LISP-a , do pracy w jego Laboratorium Sztucznej Inteligencji . Gordon pracował w Cambridge University Computer Laboratory od 1981 roku, początkowo jako wykładowca, awansował na Docent w 1988 i profesor w 1996.

został wybrany członkiem Towarzystwa Królewskiego , aw 2008 roku z okazji jego 60. urodzin odbyło się tam dwudniowe spotkanie badawcze poświęcone narzędziom i technikom weryfikacji infrastruktury systemowej .

Mike Gordon był żonaty z Avrą Cohn, doktorantką Robina Milnera na Uniwersytecie w Edynburgu i razem prowadzili badania.

Zmarł w Cambridge po krótkiej chorobie i pozostawił żonę i dwóch synów.

Praca

Gordon kierował rozwojem dowodu twierdzenia HOL . System HOL jest środowiskiem do interaktywnego dowodzenia twierdzeń w logice wyższego rzędu . Jego najbardziej wyjątkową cechą jest wysoki stopień programowalności poprzez metajęzyk ML . System ma wiele zastosowań, od formalizowania czystej matematyki po weryfikację sprzętu przemysłowego.

Odbyła się seria międzynarodowych konferencji na temat systemu HOL, TPHOLs. Pierwsze trzy były nieformalnymi spotkaniami użytkowników bez opublikowanych materiałów. Tradycją jest teraz coroczna konferencja na kontynencie innym niż miejsce poprzedniego spotkania. Od 1996 roku zakres rozszerzył się, obejmując wszystkie dowody twierdzeń w logice wyższego rzędu.

Linki zewnętrzne

• Strona główna Mike'a Gordona