SSA is Freyd Categories
summary
Claim: SSA without control-flow equals Freyd categories; SSA with DAG control-flow equals distributive Freyd categories; general control-flow is a distributive Freyd category plus an Elgot fixpoint structure. The work builds an inductive IR called isotope-SSA, gives a categorical semantics that proves semantic substitution and congruence, models optimizations (strength reduction, constant propagation, GVN, loop hoisting, E-graph rewriting) as semantics-preserving, constructs models up to a simple TSO-style weak memory example, and reports a partial Lean4 formalization and a concrete we block device for graphs.
AI-written summary · about
chapters (10)
- 0:00SSA and Freyd categories
- 1:28Why SSA is widely used
- 3:36Freyd categories
- 5:22Semantics of basic blocks
- 7:06Control flow with co-products
- 8:31Elgot structure and loops
- 9:55General graphs with W-blocks
- 11:41Elgot category models
- 12:22Benefits of SSA optimizations
- 13:31Q&A
related talks
36mSound and Complete Refinement for SSA with Substructural Effects
26mSSA Translation Is an Abstract Interpretation
22mMechanised Semantics for Gated Static Single Assignment
19mSSA without Dominance for Higher-Order Programs
28mSSA CFG Yul A new viaIR backend
29mA Flow-Insensitive-Complete Program Representation
27mBig Steps in Higher-Order Mathematical Operational Semantics
01h 05mControl Flow Obfuscation for Featherweight Java + Efficient Fair Conjunction