On proving syntactic properties of CPS programs

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.