Sound and Complete Refinement for SSA with Substructural Effects
summary
A denotational model for SSA is given and a syntactic refinement relation is defined that is proven sound and complete against postset-enriched categories, so any non-derivable refinement has a model refuting it. The calculus adds a directed substructural effect system (polarity and multiplicity decide when effects can be duplicated, dropped or moved), an iteration-oriented language lambda I with translations to/from SSA, categorical semantics via Elgot/primoidal/fried structure, models for release‑acquire weak memory, UB, SC concurrency, and a partial formalized in Lean development.
AI-written summary · about
chapters (15)
- 0:00SSA refinement research intro
- 1:57Inductive SSA theory
- 5:48Denotational semantics
- 7:57Static Single Assignment form
- 11:31Dominance and scoping
- 16:33SSA refinement challenges
- 18:19Lambda I language intro
- 20:10Lambda I core constructs
- 21:17Effectful substitution rules
- 24:30Pair operations monoidal
- 26:19Adding control flow
- 27:23Iteration Elgot semantics
- 30:54Soundness completeness
- 31:58Optimizations memory models
- 33:11Q&A
related talks
18mSSA is Freyd Categories
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
26mSSA Translation Is an Abstract Interpretation
15mStable Relations and Abstract Interpretation of Higher-Order Programs
14mAdequacy for Algebraic Effects Revisited
22mMechanised Semantics for Gated Static Single Assignment
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
19mCombining Dependency, Grades, and Adjoint Logic