Linear-use CPS translations in the enriched effect calculus

Jeff Egger, Rasmus Møgelberg, Alexander Simpson

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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.
Original languageEnglish
Article number2
Pages (from-to)1-27
Number of pages27
JournalLogical Methods in Computer Science
Volume8
Issue number4
Publication statusPublished - 2012

Fingerprint

Dive into the research topics of 'Linear-use CPS translations in the enriched effect calculus'. Together they form a unique fingerprint.

Cite this