Michael JC Gordon - Michael J. C. Gordon
Michael JC Gordon | |
---|---|
narozený |
|
28. února 1948
Zemřel | 22. srpna 2017
Cambridge , Anglie
|
(ve věku 69)
Národnost | britský |
Státní občanství | Spojené království |
Alma mater |
Gonville and Caius College, Cambridge University of Edinburgh |
Známý jako | Prověřovač HOL teorém |
Vědecká kariéra | |
Pole | Počítačová věda |
Instituce |
Stanford University University of Cambridge |
Teze | Hodnocení a denotace čistých programů LISP: zpracovaný příklad v sémantice (1973) |
Doktorský poradce | Rod Burstall |
Michael John Caldwell Gordon FRS (28. února 1948 - 22. srpna 2017) byl přední britský počítačový vědec .
Život
Mike Gordon se narodil v Ripon , Yorkshire , Anglie . Navštěvoval Dartington Hall School a Bedales School . V roce 1966 byl přijat ke studiu inženýrství na Gonville a Caius College , University of Cambridge , ale přešel na matematiku . Během studií v roce 1969 pracoval v létě v National Physical Laboratory v Londýně a získal první kontakt s počítači.
Gordon studoval doktorát na univerzitě v Edinburghu pod dohledem Roda Burstalla a v roce 1973 zakončil diplomovou prací Evaluation and Denotation of Pure LISP Programs . Byl pozván na Stanford University v Kalifornii od Johna McCarthyho , vynálezce LISP , pracovat v jeho laboratoře umělé inteligence tam. Gordon pracoval na počítačové univerzitě v Cambridgi od roku 1981, původně jako přednášející, v roce 1988 povýšen na Readera a v roce 1996 na profesora .
V roce 1994 byl zvolen členem Královské společnosti a v roce 2008 se zde konalo dvoudenní výzkumné setkání o nástrojích a technikách pro ověřování systémové infrastruktury na počest jeho 60. narozenin.
Mike Gordon byl ženatý s Avrou Cohn , doktorandkou Robina Milnera na univerzitě v Edinburghu , a společně se pustili do výzkumu.
Zemřel v Cambridge po krátké nemoci a zůstala po něm manželka a dva synové.
Práce
Gordon vedl vývoj HOL věty prover . Hol systém je prostředí pro interaktivní dokazování vět v logice vyššího řádu . Jeho nejvýraznější vlastností je vysoký stupeň programovatelnosti prostřednictvím metajazykového ML . Systém má široké spektrum použití, od formalizace čisté matematiky po ověření průmyslového hardwaru.
Uskutečnila se řada mezinárodních konferencí o systému HOL, TPHOL. První tři byly neformální schůzky uživatelů bez publikovaných sborníků. Nyní je tradicí každoroční konference na jiném kontinentu, než je místo předchozího setkání. Od roku 1996 se rozsah rozšířil, aby pokryl všechny věty dokazující v logikách vyšších řádů.