1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University2 unknown
We shoe that, in a language wihg general continuation-effects, the syntactic, or intensional, CPS transform is mirrored by a semantic, or extensional, functional term. In other words, form only the observable behavior any direct-style term (possibly containing the usual first-class continuation primitives), we can uniformly extract the observable behavior of its CPS counterpart. As a consequence of this result, we show that the computational lambda-calculus is complete for observational equivalence of pure, simply typed lambda-terms in Scheme-like contexts.
Third Acm Sigplan Workshop on Continuations, 2001, p. 41-46