Linear-use CPS translations in the Enriched Effect Calculus

TL;DR

This paper investigates linear-use CPS translations within the enriched effect calculus (EEC), demonstrating their involutive nature and establishing full completeness results for various translation strategies.

Contribution

It introduces a unified generic translation of EEC into itself that generalizes existing CPS translations and proves its involutive property, advancing understanding of linear logic embeddings.

Findings

Established that call-by-value and call-by-name translations land in EEC fragment

Proved the generic translation of EEC is involutive up to isomorphism

Achieved full completeness results for the translations

Abstract

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.