License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2019.7
URN: urn:nbn:de:0030-drops-107997
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10799/
Go to the corresponding LIPIcs Volume Portal

Misonizhnik, Aleksandr ; Mordvinov, Dmitry

On Satisfiability of Nominal Subtyping with Variance

pdf-format:
LIPIcs-ECOOP-2019-7.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{misonizhnik_et_al:LIPIcs:2019:10799,
  author =	{Aleksandr Misonizhnik and Dmitry Mordvinov},
  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 =	{Alastair F. Donaldson},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10799},
  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}
}

Keywords: nominal type systems, structural subtyping, first-order logic, decidability, software verification
Collection: 33rd European Conference on Object-Oriented Programming (ECOOP 2019)
Issue Date: 2019
Date of publication: 10.07.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI