SSA as Freyd Categories - Categorical Semantics for Compiler Design

Explore the fundamental connection between Static Single Assignment (SSA) and Freyd categories in this insightful conference talk from GALOP'24. Delve into the mathematical foundations of modern compiler design as Jad Elkhaleq Ghalayini presents a novel perspective on SSA's wide applicability across various domains. Discover how SSA without control-flow relates to Freyd categories and learn about its graphical representation using string diagrams. Examine the correspondence between SSA with terminating control-flow and distributive Freyd categories, as well as the relationship between general control-flow SSA and Elgot structures. Gain insights into the type-theoretic presentation of isotope-SSA and its categorical semantics, understanding how various optimizations align with this framework. Explore models exhibiting interesting features, including a simple model of TSO-style weak memory. If time permits, learn about the generalization of the IR to support substructural types and impure substitutions, with potential applications in separation logic, quantum computing, and nondeterminism.

[GALOP'24] SSA is Freyd Categories