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:8949@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20260219T110000
DTEND;TZID=Europe/Paris:20260219T123000
DTSTAMP:20260205T180959Z
URL:https://www.i2m.univ-amu.fr/evenements/ohana-trees-taylor-expansion-an
 d-multi-type-semantics-for-the-%ce%bbi-calculus-no-variable-gets-left-behi
 nd-or-forgotten/
SUMMARY:Rémy Cerda (Università di Bologna): Ohana trees\, Taylor expansio
 n and multi-type semantics for the λI-calculus. No variable gets left beh
 ind or forgotten!
DESCRIPTION:Rémy Cerda: The standard notion of evaluation trees for the λ
 -calculus\, namely\nBöhm trees\, is quite ill-behaved with respect to the
  inputs of\nprograms\, namely free variables: even in the λI-calculus (th
 e\nλ-calculus without erasure)\, fv(BT(M)) = fv(BT(N)) does not give any\
 ninformation on how to compare fv(M) and fv(N). To circumvent this we\nint
 roduce a previously unknown theory of the λI-calculus\, induced by\na not
 ion of evaluation trees that we call “Ohana trees”. The Ohana\ntree of
  a λI-term is an annotated version of its Böhm tree\,\nremembering all f
 ree variables that are hidden behind a meaningless\nsubterm\, or pushed i
 nto infinity along its infinite branches. We\ndevelop the associated theor
 ies of continuous and linear\napproximation. We also characterise this the
 ory by means of a\nmulti-type system suggesting a new denotational semanti
 cs for the\nλI-calculus (as well as longer-term objectives related to\ntr
 ansfinite rewriting).
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:STANDARD
DTSTART:20251026T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR