Ohana trees, linear approximation and multi-types for the $\lambda$I-calculus: No variable gets left behind or forgotten!

Rémy Cerda, Giulio Manzonetto, Alexis Saurin

Although the $\lambda$I-calculus is a natural fragment of the $\lambda$-calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The r…