Date: Thursday, February 5 2026 – 13h00
Place: A008
Title: Thin spans and their modelling of rigid intersection types
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.