Blogs (9) >>
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Thu 3 Nov 2016 14:45 - 15:10 at Matterhorn 2 - Principles, Across the Compilation Stack Chair(s): Adam Chlipala

Scala’s type system unifies aspects of ML modules, object- oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. Unfortunately, type soundness has only been established for restricted subsets of DOT. In fact, it has been shown that important Scala features such as type refinement or a subtyping relation with lattice structure break at least one key metatheoretic property such as environment narrowing or invertible subtyping transitivity, which are usually required for a type soundness proof.
The main contribution of this paper is to demonstrate how, perhaps surprisingly, even though these properties are lost in their full generality, a rich DOT calculus that includes recursive type refinement and a subtyping lattice with intersection types can still be proved sound. The key insight is that subtyping transitivity only needs to be invertible in code paths executed at runtime, with contexts consisting entirely of valid runtime objects, whereas inconsistent subtyping contexts can be permitted for code that is never executed.

Thu 3 Nov

13:30 - 15:10: OOPSLA - Principles, Across the Compilation Stack at Matterhorn 2
Chair(s): Adam ChlipalaMIT CSAIL
splash-2016-oopsla147817620000013:30 - 13:55
Davide AnconaUniversity of Genova, Andrea Corradi
splash-2016-oopsla147817770000013:55 - 14:20
Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Tillmann RendelUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
splash-2016-oopsla147817920000014:20 - 14:45
Stephen KellUniversity of Cambridge, Dominic P. MulliganUniversity of Cambridge, Peter SewellUniversity of Cambridge
splash-2016-oopsla147818070000014:45 - 15:10
Tiark RompfPurdue University, USA, Nada AminEPFL
DOI Pre-print