Nominal type systems with variance form a core of subtype relation
in lots of object-oriented programming languages. Early studies [1] have
shown the undecidability of ground subtyping relation in such type
system, but several decidable fragments were provided. In the talk we
will discuss the *satisfiability* problem of nominal type systems
with variance: we'll define the corresponding first-order theory, show
its practical significance, demonstrate it on some tricky examples and
prove undecidability of its tiny fragment.

Supplementary materials:

[1] Kennedy, Andrew J. and Benjamin C. Pierce. On Decidability of Nominal Subtyping with Variance. (2006).

Presenter: Dmitry Mordvinov

Date: October 22, 2018

Time: 17:15

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28