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