Naissance | |
---|---|
Décès |
(à 77 ans) États-Unis |
Nationalité | |
Formation |
Université Harvard |
Activités |
A travaillé pour | |
---|---|
Membre de | |
Directeurs de thèse | |
Distinction |
médaille Lovelace (2010) |
John Charles Reynolds ( – ) est un informaticien américain[1]. Il est réputé pour ses contributions à la théorie de la programmation.
John Reynolds étudie à l'université Purdue (1953-56) où il obtient un B. Sc. et à l'université Harvard (1956-61). Il obtient en 1961 un Ph. D. en physique théorique avec une thèse intitulée « Surface Properties of Nuclear Matter »[2]. Il travaille ensuite au Laboratoire national d'Argonne (1961-1970). Il s'intéresse à la programmation et à ses fondements logiques. Il est professeur en sciences de l'information à l'université de Syracuse de 1970 à 1986. À partir de cette date, il est professeur en informatique à l'université Carnegie-Mellon jusqu'à sa retraite en 2012, puis professeur émérite. Il a également été professeur invité à l'université d'Aarhus, à l'université d'Édimbourg, à l'Imperial College London, à Microsoft Research à Cambridge) et à la Queen Mary University of London. Il a fait plusieurs séjours en France, notamment comme chercheur invité à l'Inria en 1983-1984. Il était Invited Speaker au congrès IFIP ’83 à Paris en .
Le principal sujet de recherche de John Reynolds est le domaine des langages de programmation et des langages de spécification associés, notamment ce qui concerne leur sémantique formelle. Il a inventé le système F ou lambda-calcul polymorphe qui est une extension du lambda-calcul simplement typé introduite indépendamment par le logicien Jean-Yves Girard. Il a formulé la propriété de la paramétricité (en) sémantique. Il a écrit un article fondamental sur la définition des interprètes, qui a précisé les premiers travaux sur les continuations et a introduit la technique de défonctionalisation (en). Il a appliqué la théorie des catégories à la sémantique des langages de programmation. Il a défini les langages de programmation Gedanken et Forsythe, et est connu pour son emploi des types d'intersection en sous-typage. Il a travaillé sur la logique de séparation qui permet de décrire et d'analyser des structures de données mutables partagées.
John Reynolds a été éditeur des Communications of the ACM et du Journal of the ACM.