Delia Kesner - A Theory of Explicit Substitutions with Safe and Full Composition

lmcs:816 - Logical Methods in Computer Science, July 15, 2009, Volume 5, Issue 3 - https://doi.org/10.2168/LMCS-5(3:1)2009
A Theory of Explicit Substitutions with Safe and Full Composition

Authors: Delia Kesner

    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.


    Volume: Volume 5, Issue 3
    Published on: July 15, 2009
    Accepted on: June 25, 2015
    Submitted on: December 8, 2008
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,F.3.2,D.1.1,F.4.1

    Linked data

    Source : ScholeXplorer IsCitedBy ARXIV 2111.01485
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.fscd.2021.9
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.2111.01485
    • 10.48550/arxiv.2111.01485
    • 10.4230/lipics.fscd.2021.9
    • 2111.01485
    A strong call-by-need calculus
    Balabonski, Thibaut ; Lanco, Antoine ; Melquiond, Guillaume ;

    11 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 396 times.
    This article's PDF has been downloaded 481 times.