In their 1983 paper, Barendregt, Coppo and Dezani-Ciancaglini defined an intersection type system, now known under the name BCD. This system relies on a subtyping relation, and most of the properties of BCD typing are related with properties of BCD subtyping. We thus focus on the study of BCD subtyping.

By understanding the BCD subtyping relation as a deduction relation, we propose to look at it from a proof-theoretical point of view. We give a sequent calculus presentation IS of BCD subtyping and study its core properties: cut-elimination, sub-formula property, rule inversions, beta condition, etc. Thanks to a Girard's style translation of IS, we prove that BCD subtyping can be seen as a fragment of Lambek's calculus. Finally we address ongoing work on the computational complexity of BCD subtyping, as well as alternative presentations and possible extensions.