Linearly-Used Continuations in the Enriched Effect Calculus

Jeff Egger, Rasmus Møgelberg, Alex Simpson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 call-by-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 map is an equivalence of models. Thus the initial model is self-dual.
Original languageEnglish
Title of host publicationFoundations of Software Science and Computational Structures
Subtitle of host publication13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings
EditorsLuke Ong
PublisherSpringer-Verlag GmbH
Pages18-32
Number of pages15
Volume6014
ISBN (Print)978-3-642-12031-2
DOIs
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume6014

Fingerprint

Dive into the research topics of 'Linearly-Used Continuations in the Enriched Effect Calculus'. Together they form a unique fingerprint.

Cite this