Paper Info
Title
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 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.
Year
DOI
Venue
2010
10.1007/978-3-642-12032-9_3
FoSSaCS
Field
DocType
Volume
Discrete mathematics,Time-scale calculus,Isomorphism,Equivalence (measure theory),Metalanguage,Linear logic,Completeness (statistics),Syntax,Calculus,Semantics,Mathematics
Conference
6014
ISSN
ISBN
Citations 
0302-9743
3-642-12031-8
6
PageRank 
References 
Authors
0.53
9
3
Name
Order
Citations
PageRank
Jeff Egger1282.06
Rasmus Ejlers Møgelberg220416.63
Alex Simpson311314.15