|
On proving syntactic properties of CPS programs
Olivier Danvy
August 1999 |
Abstract:
Higher-order program transformations raise new challenges for
proving properties of their output, since they resist traditional,
first-order proof techniques. In this work, we consider (1) the ``one-pass''
continuation-passing style (CPS) transformation, which is second-order, and
(2) the occurrences of parameters of continuations in its output. To this
end, we specify the one-pass CPS transformation relationally and we use the
proof technique of logical relations
Available as PostScript, PDF, DVI. |