Séminaire APR
Thin spans and their modelling of rigid intersection types
Jeudi 27 mars 2025Simon Forest (Aix Marseille Univ, CNRS, LIS)
Thins spans were recently introduced as a quantitative, or proof-relevant, model of programming languages based on spans of groupoids. As a model of linear logic, they can be seen as an extension of the relational model Rel where, in the interpretation of a program, not only some inputs are related to some outputs, but the different ways or computations a program can make to transform the given inputs to the given outputs are recorded.
In an ongoing work, we show that thin spans provide a useful model of so-called rigid intersection types, that are non-idempotent and non-commutative intersection types. It is already known that the relational model Rel can be syntactically described using a non-idempotent but commutative intersection type system. The commutativity is essential for the property of subject reduction, stating that the interpretation of a program is not changed by reduction. Nevertheless, the interpretation of programs in thin spans can be described by a rigid intersection type system, while still enjoying a relaxed subject reduction property.
In this talk, a rather light-weight presentation of thin spans will be given, followed by a presentation of the rigid intersection type system associated to them.
This is joint work with Pierre Clairambault.