A Theory of Explicit Substitutions with Safe and Full Composition

Many different systems with explicit substitutions have been proposed toimplement a large class of higher-order languages. Motivations and challengesthat guided the development of such calculi in functional frameworks aresurveyed in the first part of this paper. Then, very simple technology in namedvariable-style notation is used to establish a theory of explicit substitutionsfor the lambda-calculus which enjoys a whole set of useful properties such asfull composition, simulation of one-step beta-reduction, preservation ofbeta-strong normalisation, strong normalisation of typed terms and confluenceon metaterms. Normalisation of related calculi is also discussed.Comment: 29 pages Special Issue: Selected Papers of the Conference "International Colloquium on Automata, Languages and Programming 2008" edited by Giuseppe Castagna and Igor Walukiewic