Intersection Types are a well-known family of tools that characterise different notions of normalisation. We develop a general framework for building such systems from a notion of approximation, that allows to recover many well-known intersection type systems, as well as new systems, for every calculus that can be translated into linear logic. This construction uses in a crucial way Melliès and Zeilberger’s “type systems as functors” viewpoint, as well as an adapted Grothendieck construction.

Based on a joint work with Damiano Mazza and Pierre Vial.