Reasoning About Code-Generation in Two-Level Languages

Abstract

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
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.

- 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.

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:
one-pass transformations into continuation-passing style and
type-directed partial evaluation for call-by-name and for call-by-value.

Keywords. Two-level languages, erasure, type preservation, native implementation,
partial evaluation.