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

Abstract

This is a companion report for the OOPSLA 2023 paper of the same title, presenting a detailed end-to-end account of the $λ^*_{\mathsf{G}}$ graph IR, at a level of detail beyond a regular conference paper. Our first concern is adequacy and soundness of $λ^*_{\mathsf{G}}$, which we derive from a direct-style imperative functional language (a variant of Bao et al.'s $λ^*$-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 $λ^*_{\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 $λ^*_{\mathsf{G}}$'s equational rules that drive compiler optimizations (e.g., DCE, $λ$-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 $λ^*_{\mathsf{G}}$ in MNF in terms of previously developed logical relations for the direct-style $λ^*$-calculus. Finally, we also include a longer version of the conference paper's section on code generation and code motion for $λ^*_{\mathsf{G}}$ as implemented in Scala~LMS.