Static single assignment form, or SSA, has been the dominant compiler intermediate representation for decades. In this paper, we give a type theory for a variant of SSA, including its equational theory, which are strong enough to validate a variety of control and data flow transformations. We also give a categorical semantics for SSA, and show that the type theory is sound and complete with respect to the categorical axiomatization. We demonstrate the utility of our model by exhibiting a variety of concrete models satisfying our axioms, including in particular a model of TSO weak memory. The correctness of the syntactic metatheory, as well as the completeness proof has been mechanized in the Lean proof assistant.

翻译：静态单赋值形式（SSA）作为编译器中间表示已主导数十年。本文提出一种SSA变体的类型理论，包含其等式理论，该理论具备足够强的表达能力以验证多种控制流与数据流转换。我们同时建立了SSA的范畴语义，并证明该类型理论相对于范畴化公理体系具备可靠性与完备性。通过构建多个满足公理的具体模型（特别包括TSO弱内存模型），我们展示了该模型的实用性。语法元理论的正确性证明及完备性证明已在Lean证明助手中完成形式化验证。