Static Single Assignment (SSA) intermediate representation is widely used to optimize and compile code in imperative and object-oriented languages, but it can also be useful for static type analysis. We introduce FJSSA , a Java-like imperative calculus supporting programs in SSA form; we define its big-step operational semantics, and a judgment to statically check whether a program is in SSA form, and prove its soundness. FJSSA provides a formal basis for type analysis of programs in SSA form in object-oriented languages.
Tue 19 Jul (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
|11:00 - 11:30|
|DOI Pre-print File Attached|
|11:30 - 12:00|
|12:00 - 12:25|