Michael JC Gordon - Michael J. C. Gordon

Michael JC Gordon
ProfesörMichaelJCGordon.jpg
Doğmak ( 1948-02-28 )28 Şubat 1948
Öldü 22 Ağustos 2017 (2017-08-22)(69 yaşında)
Cambridge , İngiltere
Milliyet ingiliz
Vatandaşlık Birleşik Krallık
gidilen okul Gonville ve Caius Koleji, Cambridge
Edinburgh Üniversitesi
Bilinen HOL teoremi ispatlayıcısı
Bilimsel kariyer
Alanlar Bilgisayar Bilimi
kurumlar Stanford Üniversitesi
Cambridge Üniversitesi
Tez Saf LISP programlarının değerlendirilmesi ve anlamı: anlambilimde çalışılmış bir örnek  (1973)
Doktora danışmanı çubuk patlaması

Michael John Caldwell Gordon FRS (28 Şubat 1948 - 22 Ağustos 2017), önde gelen bir İngiliz bilgisayar bilimcisiydi .

Hayat

Mike Gordon Ripon , Yorkshire , İngiltere'de doğdu . O katıldı Dartington Hall Okulu ve Bedales Okulu . 1966 yılında okumaya hak mühendislik de Gonville ve Caius College , Cambridge Üniversitesi'nin , ancak transfer matematik . Yaptığı çalışmalar sırasında, 1969 yılında görev yaptığı National Laboratory in London bilgisayarlara ilk poz kazanıyor, yaz aylarında.

Gordon için çalışılan doktora derecesi de Edinburgh Üniversitesi tarafından denetlenen Rod Burstall başlıklı tez ile 1973 yılında bitirerek Değerlendirme ve Saf LISP Programları Anlam . O davet edildi Stanford Üniversitesi de Kaliforniya tarafından John McCarthy , mucidi LISP yaptığı çalışmaya, Yapay Zeka Laboratuvarı orada. Gordon , 1981'den itibaren Cambridge Üniversitesi Bilgisayar Laboratuvarı'nda , başlangıçta öğretim görevlisi olarak çalıştı, 1988'de Reader ve 1996'da Profesör oldu.

1994'te Royal Society üyeliğine seçildi ve 2008'de 60. doğum gününün onuruna burada Sistem Altyapısının Doğrulanması için Araçlar ve Teknikler üzerine iki günlük bir araştırma toplantısı düzenlendi.

Mike Gordon ile evliydi Avra Cohn , bir doktora öğrencisi Robin Milner de Edinburgh Üniversitesi ve birlikte bir araştırma gerçekleştirdi.

Kısa bir hastalıktan sonra Cambridge'de öldü ve karısı ve iki oğlu tarafından hayatta kaldı.

Çalışmak

Gordon, HOL teoremi ispatlayıcısının geliştirilmesine öncülük etti . HOL sistemi interaktif bir ortamdır Teorem ispatı bir de yüksek mertebeden mantık . En göze çarpan özelliği, meta dil ML aracılığıyla yüksek derecede programlanabilir olmasıdır . Sistem, saf matematiğin resmileştirilmesinden endüstriyel donanımın doğrulanmasına kadar çok çeşitli kullanımlara sahiptir.

HOL sistemi, TPHOL'ler hakkında bir dizi uluslararası konferans yapılmıştır. İlk üçü, yayınlanmış bir prosedürü olmayan gayri resmi kullanıcı toplantılarıydı. Artık gelenek, önceki toplantının konumundan farklı bir kıtada yıllık bir konferans için. 1996'dan itibaren kapsam, üst düzey mantıklarda ispatlanan tüm teoremi kapsayacak şekilde genişletildi.

Referanslar

Dış bağlantılar