BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:5327@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20241024T110000
DTEND;TZID=Europe/Paris:20241024T123000
DTSTAMP:20240919T163750Z
URL:https://www.i2m.univ-amu.fr/evenements/bohm-and-taylor-for-all/
SUMMARY:Aloÿs Dufour (LIPN\, Sorbonne Paris Nord): Böhm and Taylor for al
 l
DESCRIPTION:Aloÿs Dufour: \n\nBöhm approximations\, used in the definitio
 n of Böhm trees\, are a staple of the semantics of the lambda-calculus. I
 ntroduced more recently by Ehrhard and Regnier\, Taylor approximations pro
 vide 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 Taylo
 r approximations. Böhm and Taylor approximations are available for severa
 l variants or extensions of the lambda-calculus and\, in some cases\, comm
 utation theorems are known. In this paper\, we define Böhm and Taylor app
 roximations and prove the commutation theorem in a very general setting. W
 e also introduce (non-idempotent) intersection types at this level of gene
 rality. From this\, we show how the commutation theorem and intersection t
 ypes may be applied to any calculus embedding in a sufficiently nice way i
 nto our general calculus. All known Böhm-Taylor commutation theorems\, as
  well as new ones\, follow by this uniform construction.\n\nJoint work wit
 h Damiano Mazza.\n\n
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - TPR2\, Salle de Séminaire 304-306 (3ème étage)\, 1
 63 Avenue de Luminy\, Marseille\, 13009\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, Mars
 eille\, 13009\, France;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - TPR2\, Sall
 e de Séminaire 304-306 (3ème étage):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20240331T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR