Subtyping is a key ingredient of many intersection type systems. In the case of the BCD system, B. Pierce gave a transitivity-free presentation of subtyping. This alternative presentation provides better structural properties for the analysis of this relation and leads to a simple decision algorithm.

In this talk, I will show how this transitivity-free approach can be extended beyond BCD to a broad class of intersection type systems. The extensions we consider allow imposing some pre-order as well as fixpoint equations on atoms. This includes in particular the case of various intersection type systems compatible with eta-equality (Scott, Park, etc).

I will then establish the equivalence between these transitivity-free systems and their traditional BCD-style presentations using cut-elimination techniques from proof theory. The presence of fixpoints requires moving beyond standard finite derivations, leading to the use of non-wellfounded derivations. In the context of the structural analysis of intersection subtyping, this happens to be the first use of infinitary derivations.

This is joint work with Olivier Laurent.