My papers and resources
Subtyping delimited continuations
We present a type system with subtyping for first-class delimited continuations that generalizes Danvy and Filinski's type system for shift and reset by maintaining explicit information about the types of contexts in the metacontext. We exploit this generalization by considering the control operators known as shift0 and reset0 that can access arbitrary contexts in the metacontext. We use subtyping to control the level of information about the metacontext the expression actually requires and in particular to coerce pure expressions into effectful ones. For this type system we prove strong type soundness and termination of evaluation and we present a provably correct type reconstruction algorithm. We also introduce two CPS translations for shift0 and reset0: one targeting the untyped lambda calculus, and another - type-directed - targeting the simply-typed lambda calculus. The latter translation preserves typability and is selective in that it keeps pure expressions in direct style.
A Dynamic Interpretation of the CPS Hierarchy
The CPS hierarchy of control operators shifti/reseti of Danvy and Filinski is a natural generalization of the shift and reset static control operators that allow for abstracting delimited control in a structured and CPS-guided manner. In this article we show that a dynamic variant of shift/reset, known as shift0/reset0, where the discipline of static access to the stack of delimited continuations is relaxed, can fully express the CPS hierarchy. This result demonstrates the expressive power of shift0/reset0 and it offers a new perspective on practical applications of the CPS hierarchy.
Axiomatizing Subtyped Delimited Continuations
We present direct equational axiomatizations of the call-by-value lambda calculus with the control operators shift0 and reset0 that generalize Danvy and Filinski's shift and reset in that they allow for abstracting control beyond the top-most delimited continuation. We address an untyped version of the calculus as well as a typed version with effect subtyping. For each of the calculi we present a set of axioms that we prove sound and complete with respect to the corresponding CPS translation.