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.