TY - JOUR AU - Danvy, Olivier AU - Dzafic, Belmina AU - Pfenning, Frank PY - 1999/01/23 Y2 - 2024/03/28 TI - On proving syntactic properties of CPS programs JF - BRICS Report Series JA - BRICS VL - 6 IS - 23 SE - Articles DO - 10.7146/brics.v6i23.20092 UR - https://tidsskrift.dk/brics/article/view/20092 SP - AB - Higher-order program transformations raise new challenges for proving<br />properties of their output, since they resist traditional, first-order proof<br />techniques. In this work, we consider (1) the "one-pass" continuation-passing<br />style (CPS) transformation, which is second-order, and (2) the<br />occurrences of parameters of continuations in its output. To this end, we<br />specify the one-pass CPS transformation relationally and we use the proof<br />technique of logical relations. ER -