Denotational style correctness of a CPS-Transform based compiler
Arthur Nunes-Harwitt · RIT Scholar Works (Rochester Institute of Technology) · 2008
RIT department of computer science technical report. Correctness is a crucial property for compilers; programmers rely on it when writing code. Ideally, correctness should be proved. Work on compiler correctness has focused on direct translation strategies. However, in practice, the continuation passing style (CPS) transform (or a variant) is often used in the translation process. Here a simple source language and its CPS-transform based compiler are introduced. A tractable proof for this compiler is presented, including a denotational proof of the correctness of a CPS-transform. The benefits of the proof are discussed.