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

Санкт-Петербург, осень 2017

Описание

Мы рассмотрим проблему населенности (или обитаемости) типа для ряда типизированных систем лямбда-исчисления. Проблема формулируется так: можем ли мы по заданному типу сконструировать замкнутый терм, имеющий такой тип. Мы поговорим про алгоритмы поиска обитателя и перечисления всех обитателей для просто типизированного лямбда-исчисления, после чего обсудим вопрос, на какие более богатые системы эти алгоритмы могут быть обобщены.

Преподаватели

Список лекций