Michael JC Gordon - Michael J. C. Gordon

Michael JC Gordon
Profesor MichaelJCGordon.jpg
narozený ( 1948-02-28 )28. února 1948
Zemřel 22. srpna 2017 (2017-08-22)(ve věku 69)
Cambridge , Anglie
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ů.

Reference

externí odkazy