Исследовательская группа

Лаборатория языковых инструментов

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

October 22

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

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

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

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