In this talk, we will show how to give a denotational model for static single assignment (SSA), the dominant intermediate representation for modern production compilers, and show how it enables proving the correctness of a variety of compiler optimizations. Because SSA is an effectful programming language, with features like undefined behaviour, state, and concurrency, we need to equip our calculus with a directed notion of program refinement (an inequational theory) rather than the equational theory as with most purely functional languages. Furthermore, which refinements are sound depends on which effects are used, and whether effects are duplicated, moved, or dropped. This gives rise to a natural notion of substructural effect system for our language.