The relational semantics, and beyond

Apr 19 11:00 ₂₀₂₂

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.