Wed 17 Jul 2019 14:50 - 15:10 at Track 1 - Types

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

ecoop-2019-papers
13:30 - 15:10: ECOOP Research Papers - Types at Track 1
ecoop-2019-papers13:30 - 13:50
Research paper
Richard RobertsVictoria University of Wellington, Stefan MarrUniversity of Kent, Michael HomerVictoria University of Wellington, James NobleVictoria University of Wellington
ecoop-2019-papers13:50 - 14:10
Research paper
Jan de Muijnck-HughesUniversity of Glasgow, Wim VanderbauwhedeUniversity of Glasgow
ecoop-2019-papers14:10 - 14:30
Research paper
Alen ArslanagićUniversity of Groningen, Jorge A. PérezUniversity of Groningen, The Netherlands, Erik VoogdUniversity of Groningen
Pre-print
ecoop-2019-papers14:30 - 14:50
Research paper
Benjamin ChungNortheastern University, Francesco Zappa NardelliInria, Jan VitekNortheastern University
ecoop-2019-papers14:50 - 15:10
Research paper
Aleksandr MisonizhnikSaint-Petersburg State University, Dmitry MordvinovSaint-Petersburg State University, JetBrains Research