Projects per year
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 continuationpassingstyle (CPS) translations in which the typing of the translations enforces the linear usage of continuations. We first observe that established callbyvalue and callby name linearuse CPS translations of simplytyped lambdacalculus 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 selftranslation of EEC is involutive up to isomorphism. As corollaries, we obtain full completeness results, both for the generic translation, and for the original callbyvalue and callbyname translations.
Original language  English 

Journal  Logical Methods in Computer Science 
Volume  8 
Issue number  4 
ISSN  18605974 
Publication status  Published  2012 
Keywords
 Enriched Effect Calculus
 ContinuationPassing Style
 Linear Logic
 Generic Translation
 Involutive Transformation
Fingerprint
Dive into the research topics of 'Linearuse CPS translations in the enriched effect calculus'. Together they form a unique fingerprint.Projects
 1 Finished

Modeller og detaljerede kalkuler for eﬀekter i programmeringssprog
Møgelberg, R. E. (CoI)
01/10/2007 → 31/12/2010
Project: Research