City: Saint Petersburg Novosibirsk Kazan Language: Русский English

Type inhabitation problems and their decidability
Saint Petersburg / autumn 2017, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

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

Date and time Class|Name Venue|short Materials
25 November
17:15–18:45
Лекция 1, Lecture ПОМИ РАН slides,  video
25 November
19:00–20:30
Лекция 2, Lecture ПОМИ РАН slides,  video