Abstract

We argue 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 interpretations, as partial involutions, in a natural Geometry of Interaction model รก la Abramsky. This permits to explain in elementary terms the somewhat puzzling notion of linear application arising in Geometry of Interaction, simply as the resolution between principal types using a bottom-up, variable-occurrence oriented unification algorithm alternate to the traditional one, which is top-down.


Last modified: Wed Nov 22 22:14:17 CET 2023