A Theory of Explicit Substitutions with Safe and Full Composition

DOI10.2168/LMCS-5(3:1)2009zbMATH Open1168.68008arXiv0905.2539MaRDI QIDQ3395095FDOQ3395095

Authors: Delia Kesner 

Publication date: 20 August 2009

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

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.

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

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

Mathematics Subject Classification ID

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

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
• Simultaneous substitution in the typed lambda calculus
• Title not available (Why is that?)
• 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
• Term Rewriting and Applications
• \(\lambda\)-calculi with explicit substitutions and composition which preserve \(\beta\)-strong normalization
• 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
• Title not available (Why is that?)
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Title not available (Why is that?)
• 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)