On proving syntactic properties of CPS programs

  • Olivier Danvy
  • Belmina Dzafic
  • Frank Pfenning


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.
How to Cite
Danvy, O., Dzafic, B., & Pfenning, F. (1999). On proving syntactic properties of CPS programs. BRICS Report Series, 6(23). https://doi.org/10.7146/brics.v6i23.20092