A Theory of Explicit Substitutions with Safe and Full Composition

DOI10.2168/LMCS-5(3:1)2009MaRDI QIDQ3395095zbMATH OpenFDO

Authors Delia Kesner

Publication date 20 August 2009

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0905.2539

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

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.

Recommendations

• The Theory of Calculi with Explicit Substitutions Revisited
• \(\lambda\)-calculi with explicit substitutions preserving strong normalization
• Comparing calculi of explicit substitutions with eta-reduction
• scientific article; zbMATH DE number 1956511
• scientific article; zbMATH DE number 1500649

Cited in

(25)

• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• A flexible framework for visualisation of computational properties of general explicit substitutions calculi
• A strong bisimulation for a classical term calculus
• scientific article; zbMATH DE number 1956511 (Why is no real title available?)
• Simultaneous substitution in the typed lambda calculus
• The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
• Explicit substitutions and higher-order syntax
• The spirit of node replication
• Unification for \(\lambda\)-calculi without propagation rules
• \(\lambda\)-calculi with explicit substitutions and composition which preserve \(\beta\)-strong normalization
• Term Rewriting and Applications
• Higher-order substitutions
• The Theory of Calculi with Explicit Substitutions Revisited
• Normalisation for higher-order calculi with explicit substitutions
• Node Replication: Theory And Practice
• Delayed Substitutions
• On explicit substitution with names
• scientific article; zbMATH DE number 4182831 (Why is no real title available?)
• Exponentials as substitutions and the cost of cut elimination in linear logic
• scientific article; zbMATH DE number 7155170 (Why is no real title available?)
• An abstract factorization theorem for explicit substitutions
• ON STEPWISE EXPLICIT SUBSTITUTION
• CINNI -- a generic calculus of explicit substitutions and its application to \(\lambda\)-, \(\sigma\)- and \(\pi\)-calculi
• SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi
• Canonicity of proofs in constructive modal logic

This page was built for publication: A Theory of Explicit Substitutions with Safe and Full Composition

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3395095)