1 Search Results for "Mordvinov, Dmitry"

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)

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

  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-dev.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}
  • Refine by Author
  • 1 Misonizhnik, Aleksandr
  • 1 Mordvinov, Dmitry

  • Refine by Classification
  • 1 Software and its engineering → Automated static analysis
  • 1 Software and its engineering → Inheritance
  • 1 Software and its engineering → Object oriented languages
  • 1 Software and its engineering → Polymorphism
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 1 decidability
  • 1 first-order logic
  • 1 nominal type systems
  • 1 software verification
  • 1 structural subtyping

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2019

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail