Speaker: Giulio Manzonetto, LIPN.

Tuesday 19 April 2022, 10:00, (room 1Z71 ENS Paris-Saclay and online)

**Abstract:**
Since the pioneering work by Barendregt, Dezani-Ciancaglini
and Coppo, some models of lambda-calculus are based on filters and can
be presented as intersection type systems. The interpretation of a
program in these models is just the set of its types, which is a
filter. Filter models can be used to capture operational properties of
programs like normalization, head normalization, or solvability, but
establishing these results often requires impredicative techniques
like Girard's reducibility candidates. In this talk we present a more
recent class of models, called relational models and arising from a
simple quantitative semantics of linear logic (LL). We show that these
models can be presented as intersection type systems where the
intersection operator is however non-idempotent. Due to the resource
sensitive nature of LL , we are able to capture operational properties
bypassing impredicative techniques. Starting for the type of a
program, it is indeed possible to extract an upper bound to the amount
of steps needed to reach its value. We will see that generalizing this
semantics from the Boolean semiring to continuous semi-ring allows to
compare programs not only with respect to "what they can do", but also
"in how many steps" or "in how many different ways" (for
non-deterministic PCF) or even "with what probability" (for
probabilistic PCF). Finally, generalizing relations to the
higher-dimension (profunctors) allows us to obtain the
characterization of the theory of a model as a simple corollary of the
Approximation Theorem.