General (intuitionistic or classical) proofs can be approximated arbitrarily well by linear proofs, that is, proofs that use each of their premises exactly once. In this work, we show that such linear approximations give rise, through an adapted Grothendieck construction, to intersection type systems for any logical system that can be embed meaningfully into linear logic.

We recover in this way all well-known intersection type systems, capturing different notions of normalization for various languages, and give a blueprint to compute new ones.

Joint work with Damiano Mazza and Pierre Vial.