On proving syntactic properties of CPS programs

Olivier Danvy
Belmina Dzafic
Frank Pfenning

August 1999


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.


Last modified: 2003-06-08 by webmaster.