Context-based proofs of termination for typed delimited-control operators

Abstract

We present direct proofs of termination of evaluation for typed delimited-control operators shift and reset using a variant of Tait's method with context-based reducibility predicates. We address both call by value and call by name, and for each reduction strategy we consider a type-and-effect system a la Danvy and Filinski as well as a system with a fixed answer type. The call-by-value type-and-effect system we present is a refinement of Danvy and Filinski's original type system, whereas the call-by-name type-and-effect system is new. From the normalization proofs, we extract call-by-value and call-by-name evaluators in continuation-passing style with two layers of continuations; by construction, these evaluators are instances of normalization by evaluation.