From control effects to typed continuation passing

11 years 12 months ago
From control effects to typed continuation passing
First-class continuations are a powerful computational effect, allowing the programmer to express any form of jumping. Types and effect systems can be used to reason about continuations, both in the source language and in the target language of the continuation-passing transform. In this paper, we establish the connection between an effect system for first-class continuations and typed versions of continuationpassing style. A region in the effect system determines a local answer type for continuations, such that the continuation transforms of pure expressions are parametrically polymorphic in their answer types. We use this polymorphism to derive transforms that make use of effect information, in particular, a mixed linear/non-linear continuation-passing transform, in which expressions without control effects are passed their continuations linearly. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; D.3.3 [Programming Languages]: La...
Hayo Thielecke
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where POPL
Authors Hayo Thielecke
Comments (0)