Thomas Ehrhard ; Antonio Bucciarelli ; Alberto Carraro ; Giulio Manzonetto - Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion

lmcs:1047 - Logical Methods in Computer Science, October 10, 2012, Volume 8, Issue 4 - https://doi.org/10.2168/LMCS-8(4:3)2012
Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor ExpansionArticle

Authors: Thomas Ehrhard ; Antonio Bucciarelli ; Alberto Carraro ORCID; Giulio Manzonetto

    We study the semantics of a resource-sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a "must" parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula. As an intermediate result we prove that the exception mechanism is not essential in the finite sub-calculus.


    Volume: Volume 8, Issue 4
    Published on: October 10, 2012
    Imported on: February 29, 2012
    Keywords: Computer Science - Logic in Computer Science,F.4.1

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1603 times.
    This article's PDF has been downloaded 550 times.