Blogs (9) >>
SPLASH 2016
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
objects.
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

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

13:30 - 15:10
Principles, Across the Compilation StackOOPSLA at Matterhorn 2
Chair(s): Adam Chlipala MIT CSAIL
13:30
25m
Talk
Semantic Subtyping for Imperative Object-Oriented LanguagesAEC
OOPSLA
Davide Ancona University of Genova, Andrea Corradi
DOI
13:55
25m
Talk
Parsing with First-Class DerivativesAEC
OOPSLA
Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Tillmann Rendel University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany
DOI
14:20
25m
Talk
The Missing Link: Explaining ELF Static Linking, SemanticallyAEC
OOPSLA
Stephen Kell University of Cambridge, Dominic P. Mulligan University of Cambridge, Peter Sewell University of Cambridge
DOI
14:45
25m
Talk
Type Soundness for Dependent Object Types (DOT)AEC
OOPSLA
Tiark Rompf Purdue University, USA, Nada Amin EPFL
DOI Pre-print