A Theory of Explicit Substitutions with Safe and Full Composition

Abstract

Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the first part of this paper. Then, very simple technology in named variable-style notation is used to establish a theory of explicit substitutions for the lambda-calculus which enjoys a whole set of useful properties such as full composition, simulation of one-step beta-reduction, preservation of beta-strong normalisation, strong normalisation of typed terms and confluence on metaterms. Normalisation of related calculi is also discussed.

29 pages Special Issue: Selected Papers of the Conference "International Colloquium on Automata, Languages and Programming 2008" edited by Giuseppe Castagna and Igor Walukiewicz

References in corpus (1)

• Milner's Lambda-Calculus with Partial Substitutions

Cited by in corpus (11)

• Non-idempotent intersection types and strong normalisation
• Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
• Reduction Monads and Their Signatures
• A strong call-by-need calculus
• Distilling Abstract Machines (Long Version)
• Signatures and models for syntax and operational semantics in the presence of variable binding
• Non-idempotent types for classical calculi in natural deduction style
• Swapping: a natural bridge between named and indexed explicit substitution calculi
• Explicit Weakening
• A Formalized Extension of the Substitution Lemma in Coq
• An Interactive Proof of Termination for a Concurrent $\lambda$-calculus with References and Explicit Substitutions