Sciweavers

Share
FOSSACS
2010
Springer

Linearly-Used Continuations in the Enriched Effect Calculus

9 years 2 months ago
Linearly-Used Continuations in the Enriched Effect Calculus
Abstract. The enriched effect calculus is an extension of Moggi's computational metalanguage with a selection of primitives from linear logic. In this paper, we present an extended case study within the enriched effect calculus: the linear usage of continuations. We show that established call-by-value and call-by name linearly-used CPS translations are uniformly captured by a single generic translation of the enriched effect calculus into itself. As a main syntactic theorem, we prove that the generic translation is involutive up to isomorphism. As corollaries, we obtain full completeness results for the original call-by-value and callby-name translations. The main syntactic theorem is proved using a category-theoretic semantics for the enriched effect calculus. We show that models are closed under a natural dual model construction. The canonical linearly-used CPS translation then arises as the unique (up to isomorphism) map from the syntactic initial model to its own dual. This ma...
Jeff Egger, Rasmus Ejlers Møgelberg, Alex S
Added 02 Sep 2010
Updated 02 Sep 2010
Type Conference
Year 2010
Where FOSSACS
Authors Jeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson
Comments (0)
books