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

lmcs:923 - Logical Methods in Computer Science, October 5, 2012, Volume 8, Issue 4
Linear-use CPS translations in the Enriched Effect Calculus

Authors: Egger, Jeff and Møgelberg, Rasmus Ejlers and Simpson, Alex

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.


Source : oai:arXiv.org:1209.4268
DOI : 10.2168/LMCS-8(4:2)2012
Volume: Volume 8, Issue 4
Published on: October 5, 2012
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 52 times.
This article's PDF has been downloaded 7 times.