Rencontre, 11 mai 2023

Programme

10:30 – 12:00

Gabriele Vanoni (INRIA Sophia Antipolis)

Invited talk: Monadic Intersection Types

We extend intersection types to a computational lambda-calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational semantics, but also in the type system. Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting.

Joint work with Francesco Gavazzo and Riccardo Treglia

13:45 – 14:45

Adrienne Lancelot (LIX, École Polytechnique)

Invited talk: Normal Form Bisimulations by Value

Sangiorgi's normal form bisimilarity is call-by-name, identifies all the call-by-name meaningless terms, and rests on open terms in its definition. The literature contains a normal form bisimilarity for the call-by-value λ-calculus, Lassen's enf bisimilarity, which validates all of Moggi's monadic laws. The starting point of this work is the observation that enf bisimilarity is not the call-by-value equivalent of Sangiorgi's, because it does not identify the call-by-value meaningless terms. The issue has to do with open terms. We then develop a new call-by-value normal form bisimilarity, deemed net bisimilarity, by exploiting an existing formalism for dealing with open terms in call-by-value. It turns out that enf and net bisimilarities are incomparable, as net bisimilarity identifies meaningless terms but it does not validate Moggi's laws. Moreover, there is no easy way to merge them. To better understand the situation, we provide a detailed analysis of the rich range of possible call-by-value normal form bisimilarities, relating them to Ehrhard's call-by-value relational semantics.

15:15 – 16:15

Axel Kerinec (LIPN)

Invited talk: Why Are Proofs Relevant in Proof-Relevant Models?

Relational models of lambda-calculus can be presented as type systems, the relational interpretation of a lambda-term being given by the set of its typings. Within a distributors-induced bicategorical semantics generalizing the relational one, we identify the class of ‘categorified’ graph models and show that they can be presented as type systems as well. We prove that all the models living in this class satisfy an Approximation Theorem stating that the interpretation of a program corresponds to the filtered colimit of the denotations of its approximants.

As in the relational case, the quantitative nature of our models allows to prove this property via a simple induction, rather than using impredicative techniques. Unlike relational models, our 2-dimensional graph models are also proof-relevant in the sense that the interpretation of a lambda-term does not contain only its typings, but the whole type derivations. The additional information carried by a type derivation permits to reconstruct an approximant having the same type in the same environment. From this, we obtain the characterization of the theory induced by the categorified graph models as a simple corollary of the Approximation Theorem: two lambda-terms have isomorphic interpretations exactly when their Böhm trees coincide.