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.
Electronic Notes in Theoretical Computer Science, 1999, Vol 26, p. 21-33
4th International Workshop on Higher Order Operational Techniques in Semantics. HOOTS '99, 1999