Nominal type systems with variance form a core of subtype relation in lots of object-oriented programming languages. Early studies  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.
 Kennedy, Andrew J. and Benjamin C. Pierce. On Decidability of Nominal Subtyping with Variance. (2006).
Presenter: Dmitry Mordvinov
Date: October 22, 2018
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28