We present an idealized intermediate language designed to investigate the translation between a functional intermediate representation and an imperative register transfer language as it occurs in the back-end of a compiler. A key feature of our language is its dual semantics: there is a functional and an imperative interpretation. The functional interpretation is equipped with a fully compositional notion of program equivalence that is useful for the integration of advanced optimizations. The imperative interpretation is close to assembly and can serve as a faithful model of a low-level (virtual) machine.
Programs on which both interpretations coincide are identified via a novel condition we call coherence. Translating between the two interpretations reduces to establishing coherence. Establishing coherence under preservation of the imperative semantics can be seen as a form of SSA construction. To establish coherence under preservation of the functional semantics it suffices to α-rename. An α-renaming that establishes coherence can be understood as a register assignment. From coherence, decidable correctness conditions for the translations between the two interpretations are derived.
The language together with its theory is implemented using the Coq proof assistant without axioms. Translations between the two interpretations are implemented as extractable, translation-validated transformations realizing SSA construction and register assignment.
Program representations in static single assignment (SSA) form have become standard in compiler construction, because the SSA condition eases the specification and implementation of program transformations.
We present a functional intermediate language that is well suited to represent programs in SSA form, and discuss requirements for a compositional notion of program equivalence. We outline what needs to be done to integrate the language into a simple compilation process and discuss challenges and directions of my master's thesis.
The work is done using the Coq proof assistant.
The slides can be downloaded here.