Marek Materzok / shift0

Back to home page

My papers and resources

Subtyping delimited continuations

Marek Materzok, Dariusz Biernacki
International Conference on Functional Programming (ICFP'11)

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

Marek Materzok, Dariusz Biernacki
Asian Symposium on Programming Languages and Systems (APLAS'12)

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

Marek Materzok
Computer Science Logic (CSL'13)

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.

Important papers

A Functional Abstraction of Typed Contexts

Olivier Danvy and Andrzej Filinski
DIKU Rapport 89/12, 1989

A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations

Dariusz Biernacki, Olivier Danvy, Kevin Millikin
Technical Report BRICS RS-05-16, 2005

A Static Simulation of Dynamic Delimited Control

Chung-chieh Shan
Higher Order and Symbolic Computation, 20(4), 2007

A Monadic Framework for Delimited Continuations

R. Kent Dybvig, Simon Peyton Jones, Amr Sabry
Journal of Functional Programming, 17(6), 2007

A Substructural Type System for Delimited Continuations

Oleg Kiselyov, Chung-chieh Shan
Typed Lambda Calculi and Applications (TLCA'07)