@article{Yang_2000, title={Reasoning About Code-Generation in Two-Level Languages}, volume={7}, url={https://tidsskrift.dk/brics/article/view/20213}, DOI={10.7146/brics.v7i46.20213}, abstractNote={<p>We show that two-level languages are not only a good tool for describing code-generation algorithms, but a good tool for reasoning about them<br />as well. Indeed, some general properties of two-level languages capture common proof obligations of code-generation algorithms in the form of two-level programs.<br /></p><p>- To prove that the generated code behaves as desired, we use an erasure property, which equationally relates the generated code to an erasure of the original two-level program in the object language, thereby reducing the two-level proof obligation to a simpler one-level obligation.</p><p><br />- To prove that the generated code satisfies certain syntactic constraints, e.g., that it is in some normal form, we use a type-preservation property for a refined type system that enforces these constraints.</p><p><br />In addition, to justify concrete implementations of code-generation algorithms in one-level languages, we use a native embedding of a two-level language into a one-level language. We present two-level languages with these properties both for a call-by-name object language and for a call-by-value object language with computational effects. Indeed, it is these properties that guide our language design in the call-by-value case. We consider two classes of non-trivial applications:<br />one-pass transformations into continuation-passing style and<br />type-directed partial evaluation for call-by-name and for call-by-value.</p><p>Keywords. Two-level languages, erasure, type preservation, native implementation,<br />partial evaluation.</p>}, number={46}, journal={BRICS Report Series}, author={Yang, Zhe}, year={2000}, month={Jun.} }