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.

翻译：本报告是OOPSLA 2023同名论文的配套报告，以超越常规会议论文的详细程度，全面端到端地阐述了$\lambda^*_{\mathsf{G}}$图IR。我们的首要关注点是$\lambda^*_{\mathsf{G}}$的充分性与可靠性——我们通过一系列保类型翻译，将其从直接风格的命令式函数式语言（Bao等人带可达类型和简单效应系统的$\lambda^*$-演算变体）转化为单子范式（MNF）中的演算。静态可达类型与效应完全指导了$\lambda^*_{\mathsf{G}}$的依赖综合。我们通过证明其函数性质以及依赖安全性（借助基于检查效应观测顺序的按值调用（CBV）归约的推进与保型引理）来论证其充分性。第二个关注点是：通过使用逻辑关系证明语境等价性，确立驱动编译器优化（如DCE、$\lambda$提升等）的$\lambda^*_{\mathsf{G}}$等式规则的正确性。一个关键洞见是：依赖综合的函数性质允许基于先前为直接风格$\lambda^*$-演算开发的逻辑关系，在MNF中为$\lambda^*_{\mathsf{G}}$建立逻辑关系。最后，我们还附上了会议论文中关于$\lambda^*_{\mathsf{G}}$代码生成与代码移动部分的扩展版本（该部分已在Scala LMS中实现）。