Explicit substitutions
M. Abadi, Luca Cardelli, Pierre-Louis Curien, Jean-Jacques Lévy · Journal of Functional Programming · 1991
Abstract The λσ-calculus is a refinement of the λ-calculus where substitutions are manipulated explicitly. The λσ-calculus provides a setting for studying the theory of substitutions, with pleasant mathematical properties. It is also a useful bridge between the classical λ-calculus and concrete implementations.