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 Times are displayed in time zone: Greenwich Mean Time : Belfast change
13:30 - 13:50 Research paper | Transient Typechecks are (Almost) Free Research Papers Richard RobertsVictoria University of Wellington, Stefan MarrUniversity of Kent, Michael HomerVictoria University of Wellington, James NobleVictoria University of Wellington DOI Media Attached | ||
13:50 - 14:10 Research paper | A Typing Discipline for Hardware Interfaces Research Papers DOI Media Attached | ||
14:10 - 14:30 Research paper | Minimal Session Types Research Papers Alen ArslanagićUniversity of Groningen, Jorge A. PérezUniversity of Groningen, The Netherlands, Erik VoogdUniversity of Groningen DOI Media Attached | ||
14:30 - 14:50 Research paper | Julia's Efficient Algorithm for Subtyping Unions and Covariant Tuples Research Papers Benjamin ChungNortheastern University, Francesco Zappa NardelliInria, Jan VitekNortheastern University DOI Media Attached | ||
14:50 - 15:10 Research paper | On Satisfiability of Nominal Subtyping with Variance Research Papers Aleksandr MisonizhnikSaint-Petersburg State University, Dmitry MordvinovSaint-Petersburg State University, JetBrains Research DOI Media Attached |