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
11:00
30m
Talk
A Mechanical Soundness Proof for Subtyping Over Recursive Types
FTfJP
Timothy Jones Victoria University of Wellington, David J. Pearce Victoria University of Wellington
DOI Pre-print File Attached
11:30
30m
Talk
A formal account of SSA in Java-like languages
FTfJP
Davide Ancona University of Genova, Andrea Corradi
12:00
25m
Talk
A Note on the Soundness of Difference Propagation
FTfJP
Jens Dietrich Massey University, New Zealand, Nicholas Hollingum The University of Sydney, Bernhard Scholz University of Sydney, Australia