Évènement

Rémy Cerda
Università di Bologna
https://www.i2m.univ-amu.fr/perso/remy.cerda/

Date(s) : 19/02/2026   iCal
11h00 - 12h30

The standard notion of evaluation trees for the λ-calculus, namely
Böhm trees, is quite ill-behaved with respect to the inputs of
programs, namely free variables: even in the λI-calculus (the
λ-calculus without erasure), fv(BT(M)) = fv(BT(N)) does not give any
information on how to compare fv(M) and fv(N). To circumvent this we
introduce a previously unknown theory of the λI-calculus, induced by
a notion of evaluation trees that we call “Ohana trees”. The Ohana
tree of a λI-term is an annotated version of its Böhm tree,
remembering all free variables that are hidden behind a meaningless
subterm, or pushed into infinity along its infinite branches. We
develop the associated theories of continuous and linear
approximation. We also characterise this theory by means of a
multi-type system suggesting a new denotational semantics for the
λI-calculus (as well as longer-term objectives related to
transfinite rewriting).

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

Catégories

• Séminaire