Rémy Cerda
I2M, Aix-Marseille
https://www.i2m.univ-amu.fr/perso/remy.cerda/
Date(s) : 09/12/2021 iCal
11 h 00 min - 12 h 30 min
Formalisme appuyé sur la logique linéaire de Girard, le développement de Taylor de λ-termes développé par Ehrhard et Regnier a été largement utilisé comme outil d’approximation de diverses variantes du λ-calcul. De nombreux résultats découlent d’un théorème de commutation reliant la forme normale du développement de Taylor d’un terme à l’arbre de Böhm de ce terme. Ces arbres de Böhm, quant à eux, sont une notion de « forme normale infinie » de la β-réduction, et se trouvent également être les formes normales d’une version du λ-calcul infinitaire de Kennaway et al.
Cela suggère d’étendre le développement de Taylor au calcul infinitaire en question — Λ001 de son petit nom —, dont on donnera une présentation coinductive fondée sur les travaux d’Endrullis et Polonsky. Le principal résultat auquel on aboutit est la simulation de la β-réduction infinitaire par la réduction avec ressources (finitaire) du développement de Taylor. On en discutera les conséquences, lequel chantier est toujours en cours.
L’exposé sera retransmis ici :
https://greenlight.lal.cloud.math.cnrs.fr/b/lio-hdc-jef
Emplacement
Site Sud, Luminy, Ancienne BU, Salle Séminaire2 (RdC)
Catégories