Graph IRs for Impure Higher-Order Languages (Technical Report)

TL;DR

This technical report provides a detailed formal account of the $mbda^*_{4G}$ graph IR for impure higher-order languages, establishing its correctness, adequacy, and supporting compiler optimizations through formal proofs and logical relations.

Contribution

It introduces the $mbda^*_{4G}$ graph IR, proves its soundness and correctness, and demonstrates its application in compiler optimizations with formal proofs.

Findings

Proves the adequacy and soundness of $mbda^*_{4G}$.

Establishes the correctness of optimization rules via logical relations.

Includes a formal account of code generation and code motion in Scala LMS.

Abstract

This is a companion report for the OOPSLA 2023 paper of the same title, presenting a detailed end-to-end account of the $\lambda^*_{\mathsf{G}}$ graph IR, at a level of detail beyond a regular conference paper. Our first concern is adequacy and soundness of $\lambda^*_{\mathsf{G}}$, which we derive from a direct-style imperative functional language (a variant of Bao et al.'s $\lambda^*$-calculus with reachability types and a simple effect system) by a series of type-preserving translations into a calculus in monadic normalform (MNF). Static reachability types and effects entirely inform $\lambda^*_{\mathsf{G}}$'s dependency synthesis. We argue for its adequacy by proving its functional properties along with dependency safety via progress and preservation lemmas with respect to a notion of call-by-value (CBV) reduction that checks the observed order of effects. Our second concern is establishing the correctness of $\lambda^*_{\mathsf{G}}$'s equational rules that drive compiler optimizations (e.g., DCE, $\lambda$-hoisting, etc.), by proving contextual equivalence using logical relations. A key insight is that the functional properties of dependency synthesis permit a logical relation on $\lambda^*_{\mathsf{G}}$ in MNF in terms of previously developed logical relations for the direct-style $\lambda^*$-calculus. Finally, we also include a longer version of the conference paper's section on code generation and code motion for $\lambda^*_{\mathsf{G}}$ as implemented in Scala~LMS.