Michael JC Gordon- Michael J. C. Gordon
Michael JC Gordon | |
|---|---|
 | |
| Geboren |
28. Februar 1948 |
| Ist gestorben | 22. August 2017 (69 Jahre)
Cambridge , England
|
| Staatsangehörigkeit | britisch |
| Staatsbürgerschaft | Vereinigtes Königreich |
| Alma Mater |
Gonville and Caius College, Cambridge University of Edinburgh |
| Bekannt für | HOL-Theorembeweiser |
| Wissenschaftlicher Werdegang | |
| Felder | Informatik |
| Institutionen |
Stanford University University of Cambridge |
| These | Evaluation und Denotation von reinen LISP-Programmen: ein funktionierendes Beispiel in der Semantik (1973) |
| Doktoratsberater | Rod Burstall |
Michael John Caldwell Gordon FRS (28. Februar 1948 – 22. August 2017) war ein führender britischer Informatiker .
Leben
Mike Gordon wurde in Ripon , Yorkshire , England, geboren . Er besuchte die Dartington Hall School und die Bedales School . Im Jahr 1966 wurde er akzeptiert zu studieren Ingenieur an Gonville und Caius College , University of Cambridge , aber zu übertragen Mathematik . Während seines Studiums arbeitete er 1969 im Sommer am National Physical Laboratory in London , wo er erstmals mit Computern in Berührung kam.
Gordon studierte für seine Promotion an der Universität von Edinburgh , betreut von Rod Burstall , im Jahr 1973 mit einer Dissertation zum Thema Veredelung Bewertung und Bezeichnung der reinen LISP Programme . Er wurde von John McCarthy , dem Erfinder von LISP , an die Stanford University in Kalifornien eingeladen , um dort in seinem Labor für künstliche Intelligenz zu arbeiten. Gordon arbeitete ab 1981 am Computerlabor der Cambridge University , zunächst als Dozent, 1988 zum Reader und 1996 zum Professor .
Er war eine gewählte Mitglied der Royal Society in 1994 und im Jahr 2008 ein zweitägiges Forschungs Treffen auf Werkzeuge und Techniken für die Überprüfung der Systemlandschaft dort seinen 60. Geburtstag in Ehren gehalten wurde.
Mike Gordon war mit Avra Cohn verheiratet , einer Doktorandin von Robin Milner an der University of Edinburgh , und sie forschten gemeinsam.
Er starb in Cambridge nach kurzer Krankheit und hinterlässt seine Frau und zwei Söhne.
Arbeit
Gordon leitete die Entwicklung des HOL-Theorembeweisers . Das HOL-System ist eine Umgebung für den interaktiven Theorem-Beweis in einer Logik höherer Ordnung . Sein herausragendstes Merkmal ist seine hohe Programmierbarkeit durch die Metasprache ML . Das System ist vielseitig einsetzbar, von der Formalisierung reiner Mathematik bis hin zur Verifikation industrieller Hardware.
Es gab eine Reihe internationaler Konferenzen zum HOL-System, TPHOLs. Die ersten drei waren informelle Nutzertreffen ohne veröffentlichte Verfahren. Die Tradition ist jetzt eine jährliche Konferenz auf einem anderen Kontinent als dem Ort des vorherigen Treffens. Ab 1996 wurde der Anwendungsbereich erweitert, um alle Theorembeweise in Logiken höherer Ordnung abzudecken.