![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Entry tags:
Системы типизации лямбда-исчисления: видео 7 и 8 лекций
На Лекториум.тв выложено видео двух последних лекций: про полиморфные системы и их свойства.
http://www.lektorium.tv/course/?id=22797
Лекция 7.
Полиморфные системы в стиле Карри. Сильный и слабый полиморфизм. Типы в контекстах. Введение и удаление $\forall$. Проблемы разрешимости в полиморфном λ-исчислении в стиле Карри. Let-полиморфизм. Полиморфизм высших рангов. Система в стиле Чёрча. Универсальные абстракция и применение. Импредикативность. Связь между λ2 в стиле Карри и Черча. Сильная нормализация. Интерпретации $\forall$-типов. Параметричность.
Лекция 8.
Интуиционистская пропозициональная логика второго порядка. Представление стандартных пропозициональных связок в λ2. Экзистенциальные типы. Пустой тип, булев тип, произведение и сумма типов. Типы для чисел Чёрча и списков. Индуктивные типы.
Слайды в pdf доступны здесь:
http://logic.pdmi.ras.ru/csclub/courses/systemsoftypedlambdacalculi
Последнюю лекцию рассказывал (ближе к концу) в бешеном темпе, чтобы всё успеть. Надо всё-таки останавливаться в желании впихнуть побольше. Буду стараться.
Про остальные 6 вершин лямбда-куба буду рассказывать в мае (уже на Фонтанке, скорее всего).
http://www.lektorium.tv/course/?id=22797
Лекция 7.
Полиморфные системы в стиле Карри. Сильный и слабый полиморфизм. Типы в контекстах. Введение и удаление $\forall$. Проблемы разрешимости в полиморфном λ-исчислении в стиле Карри. Let-полиморфизм. Полиморфизм высших рангов. Система в стиле Чёрча. Универсальные абстракция и применение. Импредикативность. Связь между λ2 в стиле Карри и Черча. Сильная нормализация. Интерпретации $\forall$-типов. Параметричность.
Лекция 8.
Интуиционистская пропозициональная логика второго порядка. Представление стандартных пропозициональных связок в λ2. Экзистенциальные типы. Пустой тип, булев тип, произведение и сумма типов. Типы для чисел Чёрча и списков. Индуктивные типы.
Слайды в pdf доступны здесь:
http://logic.pdmi.ras.ru/csclub/courses/systemsoftypedlambdacalculi
Последнюю лекцию рассказывал (ближе к концу) в бешеном темпе, чтобы всё успеть. Надо всё-таки останавливаться в желании впихнуть побольше. Буду стараться.
Про остальные 6 вершин лямбда-куба буду рассказывать в мае (уже на Фонтанке, скорее всего).
no subject
Так надеялся в предыдущем топике, что кто нибудь выложит на трэкер какой ни будь, был бы очень признателен.
no subject
(Anonymous) 2011-04-05 11:36 am (UTC)(link)no subject
no subject
no subject
no subject
ps: вы не могли бы намекнуть ответвенным за сайты, что было бы хорошо поправить место проведения? там до сих пор хлопина указанно, в обоих местах