Reasoning About Code-Generation in Two-Level Languages

This paper shows that two-level languages are not only a good tool for describing code-generation algorithms, but a good tool for reasoning about them as well. Common proof obligations of code-generation algorithms in the form of two-level programs are captured by certain general properties of two-level languages.

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. 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. Finally, 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 computational object language. Indeed, it is these properties that guide our language design in the call-by-value case. We consider two non-trivial applications: a one-pass transformation into continuation-passing style and type-directed partial evaluation for call-by-name and for call-by-value

Abstract: