Jeff Egger ; Rasmus Ejlers Møgelberg ; Alex Simpson - Linear-use CPS translations in the Enriched Effect Calculus

lmcs:923 - Logical Methods in Computer Science, October 5, 2012, Volume 8, Issue 4 - https://doi.org/10.2168/LMCS-8(4:2)2012
Linear-use CPS translations in the Enriched Effect Calculus

Authors: Jeff Egger ; Rasmus Ejlers Møgelberg ; Alex Simpson

    The enriched effect calculus (EEC) is an extension of Moggi's computational metalanguage with a selection of primitives from linear logic. This paper explores the enriched effect calculus as a target language for continuation-passing-style (CPS) translations in which the typing of the translations enforces the linear usage of continuations. We first observe that established call-by-value and call-by name linear-use CPS translations of simply-typed lambda-calculus into intuitionistic linear logic (ILL) land in the fragment of ILL given by EEC. These two translations are uniformly generalised by a single generic translation of the enriched effect calculus into itself. As our main theorem, we prove that the generic self-translation of EEC is involutive up to isomorphism. As corollaries, we obtain full completeness results, both for the generic translation, and for the original call-by-value and call-by-name translations.


    Volume: Volume 8, Issue 4
    Published on: October 5, 2012
    Accepted on: June 25, 2015
    Submitted on: January 31, 2011
    Keywords: Computer Science - Logic in Computer Science,D.3.1,F.3.3,F.4.1

    Share

    Consultation statistics

    This page has been seen 728 times.
    This article's PDF has been downloaded 224 times.