A Simple Correctness Proof of the Direct-Style Transformation
Lasse R. Nielsen January 2002 |
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
Available as PostScript, PDF, DVI. |