deniok: (lambda cube)
[personal profile] 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 вершин лямбда-куба буду рассказывать в мае (уже на Фонтанке, скорее всего).
This account has disabled anonymous posting.
If you don't have an account you can create one now.
HTML doesn't work in the subject.
More info about formatting

Profile

deniok: (Default)
deniok

February 2022

S M T W T F S
  12345
6789101112
13141516171819
20212223 242526
2728     

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 15th, 2025 02:34 pm
Powered by Dreamwidth Studios