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

Semantic subtyping is an approach for defining sound and
complete procedures to decide subtyping for expressive types,
including union and intersection types; although it has been
exploited especially in functional languages for XML based
programming, recently it has been partially investigated in
the context of object-oriented languages, and a sound and
complete subtyping algorithm has been proposed for record
types, but restricted to immutable fields, with union and
recursive types interpreted coinductively to support cyclic
In this work we address the problem of studying semantic
subtyping for imperative object-oriented languages, where
fields can be mutable; in particular, we add read/write field
annotations to record types, and, besides union, we consider
intersection types as well, while maintaining coinductive
interpretation of recursive types. In this way, we get a richer
notion of type with a flexible subtyping relation, able to
express a variety of type invariants useful for enforcing static
guarantees for mutable objects.
The addition of these features radically changes the defi-
nition of subtyping, and, hence, the corresponding decision
procedure, and surprisingly invalidates some subtyping laws
that hold in the functional setting.
We propose an intuitive model where mutable record val-
ues contain type information to specify the values that can be
correctly stored in fields. Such a model, and the correspond-
ing subtyping rules, require particular care to avoid circularity
between coinductive judgments and their negations which,
by duality, have to be interpreted inductively.
A sound and complete subtyping algorithm is provided,
together with a prototype implementation.

Thu 3 Nov
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:10: Principles, Across the Compilation StackOOPSLA at Matterhorn 2
Chair(s): Adam ChlipalaMIT CSAIL
13:30 - 13:55
Semantic Subtyping for Imperative Object-Oriented LanguagesAEC
Davide AnconaUniversity of Genova, Andrea Corradi
13:55 - 14:20
Parsing with First-Class DerivativesAEC
Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Tillmann RendelUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
14:20 - 14:45
The Missing Link: Explaining ELF Static Linking, SemanticallyAEC
Stephen KellUniversity of Cambridge, Dominic P. MulliganUniversity of Cambridge, Peter SewellUniversity of Cambridge
14:45 - 15:10
Type Soundness for Dependent Object Types (DOT)AEC
Tiark RompfPurdue University, USA, Nada AminEPFL
DOI Pre-print