Logical Relations for Call-by-value Delimited Continuations
Logical relations, defined inductively on the structure of types,
provide a powerful tool to characterize higher-order functions.
They often enable us to prove correctness of a program transformer
written with higher-order functions concisely.
This paper demonstrates that the technique of logical relations
can be used to characterize call-by-value functions as well as delimited
continuations.
Based on the traditional logical relations for call-by-name functions,
logical relations for call-by-value functions are first defined, whose
CPS variant is
used to prove the correctness of an offline specializer for
the call-by-value lambda-calculus.
They are then modified to cope with delimited continuations
and are used to establish the correctness of an offline specializer
for the call-by-value lambda-calculus with delimited continuation
constructs, shift and reset.
This is the first correctness proof for such a specializer.
Along the development, correctness of the continuation-based and
shift/reset-based let-insertion and A-normalization is established.