Localisation

Adresses

Aix-Marseille Université
Institut de Mathématiques de Marseille (I2M) - UMR 7373
(Site Saint-Charles) 3 place Victor Hugo, Case 19, 13331 Marseille Cedex 3
(Site Luminy) Campus de Luminy - Case 907 - 13288 Marseille Cedex 9

Séminaire

Böhm and Taylor for all

Aloÿs Dufour
LIPN, Sorbonne Paris Nord
https://lipn.univ-paris13.fr/~dufour/

Date(s) : 24/10/2024   iCal
11h00 - 12h30

Böhm approximations, used in the definition of Böhm trees, are a staple of the semantics of the lambda-calculus. Introduced more recently by Ehrhard and Regnier, Taylor approximations provide a quantitative account of the behavior of programs and are well-known to be connected to intersection types. The key relation between these two notions of approximations is a commutation theorem, roughly stating that Taylor approximations of Böhm trees are the same as Böhm trees of Taylor approximations. Böhm and Taylor approximations are available for several variants or extensions of the lambda-calculus and, in some cases, commutation theorems are known. In this paper, we define Böhm and Taylor approximations and prove the commutation theorem in a very general setting. We also introduce (non-idempotent) intersection types at this level of generality. From this, we show how the commutation theorem and intersection types may be applied to any calculus embedding in a sufficiently nice way into our general calculus. All known Böhm-Taylor commutation theorems, as well as new ones, follow by this uniform construction.

Joint work with Damiano Mazza.

Emplacement
Site Sud, Luminy, TPR2, Salle de Séminaire 304-306 (3ème étage)

Catégories


Secured By miniOrange