The Denotational Semantics of SSA

Add to your list(s) Download to your calendar using vCal

• Jad Ghalayini (University of Cambridge)
• Monday 27 January 2025, 13:00-14:00
• FS07, Computer Laboratory.

If you have a question about this talk, please contact Ariadne Si Suo .

Static Single Assignment (SSA) form has been a dominant compiler intermediate representation for decades, yet it is often treated only informally. To support more rigorous reasoning about SSA , we present an inductive formulation of SSA that can be equipped with a type theory robust enough to validate a variety of control-flow and data-flow transformations. We then define a categorical semantics for SSA and show that our type theory is sound and complete with respect to this semantics.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FS07, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.