A Simple Correctness Proof of the Direct-Style Transformation

Authors

  • Lasse R. Nielsen

DOI:

https://doi.org/10.7146/brics.v9i2.21719

Abstract

We build on Danvy and Nielsen's first-order program transformation into continuation-passing style (CPS) to present a new correctness proof of the converse transformation, i.e., a one-pass transformation from CPS back to direct style. Previously published proofs were based on, e.g., a one-pass higher-order CPS transformation, and were complicated by having to reason about higher-order functions. In contrast, this work is based on a one-pass CPS transformation that is both compositional and first-order, and therefore the proof simply proceeds by structural induction on syntax.

Downloads

Published

2002-01-05

How to Cite

Nielsen, L. R. (2002). A Simple Correctness Proof of the Direct-Style Transformation. BRICS Report Series, 9(2). https://doi.org/10.7146/brics.v9i2.21719