JetBrains Research unites scientists working in challenging new disciplines

Seminar on Satisfiability Problem in Nominal Type Systems with Variance

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