Michael JC Gordon - Michael J. C. Gordon

Michael JC Gordon
ProfesseurMichaelJCGordon.jpg
Née ( 1948-02-28 )28 février 1948
Décédés 22 août 2017 (2017-08-22)(69 ans)
Cambridge , Angleterre
Nationalité Britanique
Citoyenneté Royaume-Uni
mère nourricière Gonville et Caius College, Université de Cambridge
d'Édimbourg
Connu pour prouveur du théorème HOL
Carrière scientifique
Des champs L'informatique
Établissements Université de Stanford
Université de Cambridge
Thèse Évaluation et dénotation de programmes LISP purs : un exemple travaillé en sémantique  (1973)
Conseiller de doctorat Tige éclatée

Michael John Caldwell Gordon FRS (28 février 1948 - 22 août 2017) était un informaticien britannique de premier plan .

La vie

Mike Gordon est né à Ripon , dans le Yorkshire , en Angleterre . Il a fréquenté l'école Dartington Hall et l'école Bedales . En 1966, il a été accepté pour étudier l' ingénierie au Gonville and Caius College , Université de Cambridge , mais transféré aux mathématiques . Pendant ses études, en 1969, il a travaillé au National Physical Laboratory de Londres pendant l'été, obtenant sa première exposition aux ordinateurs.

Gordon a étudié pour son doctorat à l' Université d' Edimbourg , supervisé par Rod Burstall , terminant en 1973 avec une thèse intitulée Evaluation and Denotation of Pure LISP Programs . Il a été invité à l'université de Stanford en Californie par John McCarthy , l'inventeur du LISP , pour y travailler dans son laboratoire d'intelligence artificielle . Gordon a travaillé au Cambridge University Computer Laboratory à partir de 1981, d'abord en tant que conférencier, promu lecteur en 1988 et professeur en 1996.

Il a été élu membre de la Royal Society en 1994, et en 2008, une réunion de recherche de deux jours sur les outils et techniques de vérification de l'infrastructure système s'y est tenue en l'honneur de son 60e anniversaire.

Mike Gordon était marié à Avra Cohn , une doctorante de Robin Milner à l' Université d'Édimbourg , et ils ont entrepris des recherches ensemble.

Il est décédé à Cambridge après une brève maladie et laisse dans le deuil sa femme et ses deux fils.

Travail

Gordon a dirigé le développement du prouveur de théorème HOL . Le système HOL est un environnement de démonstration interactive de théorèmes dans une logique d'ordre supérieur . Sa caractéristique la plus remarquable est son haut degré de programmabilité grâce au métalangage ML . Le système a une grande variété d'utilisations, de la formalisation des mathématiques pures à la vérification du matériel industriel.

Il y a eu une série de conférences internationales sur le système HOL, les TPHOL. Les trois premiers étaient des réunions informelles d'utilisateurs sans comptes rendus publiés. La tradition est désormais d'organiser une conférence annuelle dans un continent différent du lieu de la réunion précédente. À partir de 1996, le champ d'application s'est élargi pour couvrir tous les théorèmes prouvant dans des logiques d'ordre supérieur.

Les références

Liens externes