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.