DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2019.7

On Satisfiability of Nominal Subtyping with Variance

Authors: Aleksandr Misonizhnik and Dmitry Mordvinov

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract

Nominal type systems with variance, the core of the subtyping 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, modular verification of object-oriented code may require 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. We discuss this result in detail, as well as show one decidable fragment and a scheme for obtaining other decidable fragments.

Cite as

Aleksandr Misonizhnik and Dmitry Mordvinov. On Satisfiability of Nominal Subtyping with Variance. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{misonizhnik_et_al:LIPIcs.ECOOP.2019.7,
  author =	{Misonizhnik, Aleksandr and Mordvinov, Dmitry},
  title =	{{On Satisfiability of Nominal Subtyping with Variance}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.7},
  URN =		{urn:nbn:de:0030-drops-107997},
  doi =		{10.4230/LIPIcs.ECOOP.2019.7},
  annote =	{Keywords: nominal type systems, structural subtyping, first-order logic, decidability, software verification}
}

Search Results

Documents authored by Mordvinov, Dmitry

On Satisfiability of Nominal Subtyping with Variance

Abstract

Cite as

Thanks for your feedback!

Could not send message