Offline Partial Evaluation for Shift and Reset

This paper presents an offline partial evaluator for the lambda-calculus with the delimited continuation constructs shift and reset. Based on Danvy and Filinski's type system for shift and reset, we first present a type system that specifies well-annotated terms. We then show a specializer that receives an annotated term and produces the output in continuation-passing style (CPS). The correctness of our partial evaluator is established using the technique of logical relations. Thanks to the explicit reference to the type of continuations, we can establish the correctness using the standard proof technique of structural induction, despite the fact that the specializer itself is written in CPS. The paper also shows an efficient constraint-based binding-time analysis as well as how to extend the present work to richer language constructs, such as recursion and conditionals.