JetBrains Research — наука, меняющая мир

Семинар по проблеме выполнимости в номинальных системах типов с вариантностью

Номинальные системы типов с вариантностью --- основа отношения подтипирования в объектно-ориентированных языках. В ранних работах [1] было показано, что отношение подтипирования в таких системах типов неразрешимо даже для замкнутых типов, но были предъявлены несколько разрешимых фрагментов. В докладе будет поставлена, мотивирована и исследована задача выполнимости в номинальных системах типов с вариантностью: будет определена соответствующая теория первого порядка, показаны некоторые ее практические применения, приведены содержательные примеры, доказана неразрешимость даже очень узкого фрагмента этой теории.

Материалы к докладу:

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

Докладчик: Д.Мордвинов

22.10.2018, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28