On proving syntactic properties of CPS programs
DOI:
https://doi.org/10.7146/brics.v6i23.20092Abstract
Higher-order program transformations raise new challenges for provingproperties 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.
Downloads
Published
1999-01-23
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
Issue
Section
Articles
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.