Wed 17 Jul 2019 14:50 - 15:10 at Mancy - Types Chair(s): Davide Ancona

Nominal type systems with variance, a core of subtype relation in object-oriented programming languages like Java, C# and Scala, have been extensively studied by Kennedy and Pierce; they have shown the undecidability of the subtyping between ground types and proposed the decidable fragments of such type systems. However, precise intraprocedural analysis of object-oriented code may require a reasoning about the relations of open types. In this paper, we formalize and investigate the satisfiability problem for nominal subtyping with variance. We define the problem in the context of first-order logic. We show that, although the non-expansive ground nominal subtyping with variance is decidable, its satisfiability problem is undecidable. Our proof uses a remarkably small fragment of the type system. In fact, we demonstrate that even for the non-expansive class tables with only nullary and unary covariant and invariant type constructors, the satisfiability of quantifier-free conjunctions of positive subtyping atoms is undecidable.

Wed 17 Jul

Displayed time zone: Belfast change

13:30 - 15:10
TypesResearch Papers at Mancy
Chair(s): Davide Ancona University of Genova
13:30
20m
Research paper
Transient Typechecks are (Almost) Free
Research Papers
Richard Roberts Victoria University of Wellington, Stefan Marr University of Kent, Michael Homer Victoria University of Wellington, James Noble Victoria University of Wellington
DOI Media Attached
13:50
20m
Research paper
A Typing Discipline for Hardware Interfaces
Research Papers
Jan de Muijnck-Hughes University of Glasgow, Wim Vanderbauwhede University of Glasgow
DOI Media Attached
14:10
20m
Research paper
Minimal Session TypesPearl
Research Papers
Alen Arslanagić University of Groningen, Jorge A. Pérez University of Groningen, The Netherlands, Erik Voogd University of Groningen
DOI Media Attached
14:30
20m
Research paper
Julia's Efficient Algorithm for Subtyping Unions and Covariant TuplesPearl
Research Papers
Benjamin Chung Northeastern University, Francesco Zappa Nardelli Inria, Jan Vitek Northeastern University
DOI Media Attached
14:50
20m
Research paper
On Satisfiability of Nominal Subtyping with Variance
Research Papers
Aleksandr Misonizhnik Saint-Petersburg State University, Dmitry Mordvinov Saint-Petersburg State University, JetBrains Research
DOI Media Attached