Blogs (28) >>
ECOOP 2016
Sun 17 - Fri 22 July 2016 Rome, Italy
Tue 19 Jul 2016 11:30 - 12:00 at Belli - Session 2 Chair(s): Delphine Demange

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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:25: Session 2FTfJP at Belli
Chair(s): Delphine DemangeIRISA / University of Rennes 1
11:00 - 11:30
A Mechanical Soundness Proof for Subtyping Over Recursive Types
Timothy JonesVictoria University of Wellington, David J. PearceVictoria University of Wellington
DOI Pre-print File Attached
11:30 - 12:00
A formal account of SSA in Java-like languages
Davide AnconaUniversity of Genova, Andrea Corradi
12:00 - 12:25
A Note on the Soundness of Difference Propagation
Jens DietrichMassey University, New Zealand, Nicholas HollingumThe University of Sydney, Bernhard ScholzUniversity of Sydney, Australia