Explicit Substitutions for Objects and Functions
Delia Kesner, Pablo E. Martínez López · 1999
This paper proposes an implementation of objects and functions via a calculus with explicit substitutions which is confluent and preserves strong normalization. The source calculus corresponds to the combination of the \\sigma-calculus of Abadi and Cardelli [AC96] and the \\lambda-calculus, and the target calculus corresponds to an extension of the former calculus with explicit substitutions. The interesting feature of our calculus is that substitutions are separated -- and treated accordingly -- in two different kinds: those used to encode ordinary substitutions and those encoding invoke substitutions. When working with explicit substitutions, this differentiation is essential to encode \\lambda-calculus into \\sigma-calculus in a conservative way, following the style proposed in [AC96].