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