Aller au contenu

John C. Reynolds

Un article de Wikipédia, l'encyclopédie libre.
John Charles Reynolds
Biographie
Naissance
Décès
(à 77 ans)
États-UnisVoir et modifier les données sur Wikidata
Nationalité
Formation
Université Harvard
Activités
Autres informations
A travaillé pour
Membre de
Directeurs de thèse
Paul C. Martin (d), Kurt Gottfried (en)Voir et modifier les données sur Wikidata
Distinction

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 .

Travaux de recherche

[modifier | modifier le code]

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.

Distinctions

[modifier | modifier le code]

Sélection de publications

[modifier | modifier le code]
Livres
Articles

Notes et références

[modifier | modifier le code]
  1. Larry Fisher, « John Reynolds, 1935 – 2013 », Communications of the ACM: ACM News, USA, Association for Computing Machinery, (consulté le )
  2. (en) « John C. Reynolds », sur le site du Mathematics Genealogy Project.

Bibliographie complémentaire

[modifier | modifier le code]
  • * Olivier Danvy, Peter O’Hearn et Philip Wadler (éditeurs), « Festschrift for John C. Reynolds's 70th Birthday », Theoretical Computer Science, vol. 375, nos 1-3,‎ , p. 1-350 (DOI 10.1016/j.tcs.2006.12.024).

Article lié

[modifier | modifier le code]

Liens externes

[modifier | modifier le code]