Prix Alonzo Church 2025 : Unification de la recherche sur le lambda-calcul

Paul Blain Levy a reçu le prix Alonzo Church 2025 pour son travail novateur sur le calcul Call-by-Push-Value (CBPV). Ses recherches ont unifié les courants distincts de la recherche sur le lambda-calcul logique pur et le lambda-calcul appliqué avec effets. Le CBPV sert de cadre unificateur pour l'étude des phénomènes computationnels et logiques, notamment les effets, la polarisation, la normalisation des termes, les isomorphismes de type et les transformations de programmes. Les contributions de Levy couvrent les types de données algébriques, la sémantique opérationnelle, la sémantique dénotationnelle et les théories équationnelles, faisant progresser de manière significative la théorie sémantique du lambda-calcul et son application à la modélisation des langages de programmation.