Системы типизации лямбда-исчисления: видео 7 и 8 лекций

[deniok]

На Лекториум.тв выложено видео двух последних лекций: про полиморфные системы и их свойства.

http://www.lektorium.tv/course/?id=22797

Лекция 7.
Полиморфные системы в стиле Карри. Сильный и слабый полиморфизм. Типы в контекстах. Введение и удаление $\forall$. Проблемы разрешимости в полиморфном λ-исчислении в стиле Карри. Let-полиморфизм. Полиморфизм высших рангов. Система в стиле Чёрча. Универсальные абстракция и применение. Импредикативность. Связь между λ2 в стиле Карри и Черча. Сильная нормализация. Интерпретации $\forall$-типов. Параметричность.

Лекция 8.
Интуиционистская пропозициональная логика второго порядка. Представление стандартных пропозициональных связок в λ2. Экзистенциальные типы. Пустой тип, булев тип, произведение и сумма типов. Типы для чисел Чёрча и списков. Индуктивные типы.

Слайды в pdf доступны здесь:
http://logic.pdmi.ras.ru/csclub/courses/systemsoftypedlambdacalculi


Последнюю лекцию рассказывал (ближе к концу) в бешеном темпе, чтобы всё успеть. Надо всё-таки останавливаться в желании впихнуть побольше. Буду стараться.

Про остальные 6 вершин лямбда-куба буду рассказывать в мае (уже на Фонтанке, скорее всего).

Comments

[(Anonymous)]

http://narod.ru/disk/9355466001/csclub_moskvin_1-8.torrent.html

[ultrasonic-rocket-science.blogspot.com (from livejournal.com)]

спасибо!