Martin Hyland
# Martin Hyland

(John) Martin Elliott Hyland est professeur de logique mathématique à l'université de Cambridge et fellow du King's College de Cambridge. Ses thèmes de recherche incluent la logique mathématique, la théorie des catégories et l'informatique théorique.

## Études

Hyland a fait ses études à l'université d'Oxford où il a obtenu un doctorat en philosophie en 1975 pour une thèse intitulée Recursion Theory on the Countable Functionals supervisée par Robin Gandy.

## Recherche et carrière

Martin Hyland est surtout connu pour ses travaux sur la théorie des catégories appliquée à la logique (théorie de la démonstration récursivité), à l'informatique théorique (lambda-calcul et sémantique des langages de programmation) et à l'algèbre de dimension supérieure. En particulier, il est connu pour ses travaux sur les topos effectifs (au sein de la théorie des topos) et sur la sémantique des jeux . Parmi ses anciens doctorants il y a Eugenia $Cheng^,$ , Tom Leinster et Valeria de Paiva .

## Prix

Martin Hyland est l'un des récipiendaires, avec Samson Abramsky, Radha Jagadeesan, Pasquale Malacaria, Chih-Hao Luke Ong et Hanno Nickau, du prix Alonzo Church 2017, « pour avoir fourni une sémantique abstraite pour le calcul d'ordre supérieur par l'introduction de modèles de jeux, révolutionnant ainsi fondamentalement le domaine de la sémantique des langages de programmation, et pour l'impact de ces modèles dans les applications ».

Martin Hyland a été fait docteur honoris causa à l'université de Bath en 2015.

## Publications (sélection)

* [2021] Martin Hyland et Christine Tasson, « The linear-non-linear substitution 2-monad », Electronic Proceedings in Theoretical Computer Science, vol. 333,‎ 2021, p. 215–229 (ISSN 2075-2180, DOI 10.4204/EPTCS.333.15)
* [2006] Martin Hyland, Gordon Plotkin et John Power, « Combining effects: Sum and tensor », Theoretical Computer Science, vol. 357, $n^{os}$ 1-3,‎ 2006, p. 70–99 (DOI 10.1016/j.tcs.2006.03.013)
* [2000] J.M.E. Hyland et C.-H.L. Ong, « On Full Abstraction for PCF: I, II, and III », Information and Computation, vol. 163, $n^o$ 2,‎ 2000, p. 285–408 (DOI 10.1006/inco.2000.2917).
* [1993] Nick Benton, Gavin Bierman, Valeria de Paiva et Martin Hyland, « A term calculus for Intuitionistic Linear Logic », TLCA 1993: Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, $n^o$ 664,‎ 1993, p. 75-90.
* [1982] J.M.E. Hyland, « The Effective Topos », Studies in Logic and the Foundations of Mathematics, vol. 110,‎ 1982, p. 165–216 (DOI 10.1016/S0049-237X(09)70129-6).
* [1975] J. M. E. Hyland, « A survey of some useful partial order relations on terms of the lambda calculus », Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, Italy, March 25-27, 1975, Lecture Notes in Computer Science, vol. 37,‎ 1975, p. 83–95 (ISBN 3-540-07416-3, DOI 10.1007/BFb0029520)
