Online Partial Evaluation for Shift and Reset
This paper presents an online partial evaluator for the
lambda-calculus with the delimited continuation constructs
shift and reset.
We first give the semantics of the delimited continuation constructs
in two ways: one by writing a continuation passing style (CPS)
interpreter and the other by transforming them into CPS.
We then combine them to obtain a partial evaluator written in CPS
which produces the result in CPS.
By transforming this partial evaluator back into a direct style (DS)
in two steps, we obtain a DS to DS partial evaluator written in DS.
The correctness of the partial evaluator is not yet formally proven.
The difficulty comes from the fact that the partial evaluator is
written using shift and reset.
The method for reasoning about such programs is not yet established.
However, the development of the partial evaluator is detailed in the
paper to give a degree of confidence that it behaves as we expect.