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

Structural type systems provide an interesting alternative to the more common nominal typing scheme. Several existing languages employ structural types in some form, including Modula-3, Scala and various extensions proposed for Java. However, formalising a recursive structural type system is challenging. In particular, the need to use structural coinduction remains a hindrance for many. We formalise in Agda a simple recursive and structural type system with products and unions. Agda proves useful here because it has explicit support for coinduction and will raise an error if this is misused. The implementation distinguishes between inductively and coinductively defined types: the former corresponds to a finite representation, such as found in source code or the internals of a compiler, while the latter corresponds to a mathematical ideal with which we can coinductively define relations and proofs that are easily applied back to the inductive interpretation. As an application of this, we provide a mechanised proof of subtyping soundness against a semantic embedding of the types into Agda.

Mechanical Subtyping Slides (ftfjp16-mechanical-subtyping-slides.pdf)306KiB

Tue 19 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:25
Session 2FTfJP at Belli
Chair(s): Delphine Demange IRISA / University of Rennes 1
A Mechanical Soundness Proof for Subtyping Over Recursive Types
Timothy Jones Victoria University of Wellington, David J. Pearce Victoria University of Wellington
DOI Pre-print File Attached
A formal account of SSA in Java-like languages
Davide Ancona University of Genova, Andrea Corradi
A Note on the Soundness of Difference Propagation
Jens Dietrich Massey University, New Zealand, Nicholas Hollingum The University of Sydney, Bernhard Scholz University of Sydney, Australia