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
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
Timothy JonesVictoria University of Wellington, David PearceVictoria University of Wellington
DOI Pre-print File Attached
11:30 - 12:00
Davide AnconaUniversity of Genova, Andrea Corradi
12:00 - 12:25
Jens DietrichMassey University, New Zealand, Nicholas HollingumThe University of Sydney, Bernhard ScholzUniversity of Sydney, Australia