Projects per year
Abstract / Description of output
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.
Original language | English |
---|---|
Article number | 2 |
Pages (from-to) | 1-27 |
Number of pages | 27 |
Journal | Logical Methods in Computer Science |
Volume | 8 |
Issue number | 4 |
Publication status | Published - 2012 |
Fingerprint
Dive into the research topics of 'Linear-use CPS translations in the enriched effect calculus'. Together they form a unique fingerprint.Projects
- 1 Finished