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

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-andeffect 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. Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features—Control structures; F.3.3 [Logics and Meanings of Programs]: Semantics of Programming Languages—Studies of program const...

• Type: Conference
• Year: 2009
• Where: PPDP
• Authors: Malgorzata Biernacka, Dariusz Biernacki
• Keywords: Context-based Reducibility Predicates, PPDP 2009, Reducibility Predicates, Type System