Principal Types as Partial Involutions

Furio Honsell, Marina Lenisa, Ivan Scagnetto

We show that the principal types of the closed terms of the affine fragment of $\lambda$-calculus, with respect to a simple type discipline, are structurally isomorphic to their interpre…