Handling Delimited Continuations with Dependent Types

Dependent types are a powerful tool for maintaining non-trivial invariants, while control operators are a useful facility for implementing sophisticated behaviors. It is known that having both in a single language requires a purity restriction on type dependency, i.e., types may depend only on pure terms. In this talk, I show how to incorporate Danvy and Filinski’s shift and reset operators into a dependently typed language. The main finding is that the flexibility of shift and reset gives rise to new kinds of problematic type dependency, namely dependency of and on continuations.