Michael JC Gordon - Michael J. C. Gordon
Michael JC Gordon | |
---|---|
Doğmak |
|
28 Şubat 1948
Öldü | 22 Ağustos 2017
Cambridge , İngiltere
|
(69 yaşında)
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.