Системы типизации лямбда-исчисления. Лекция 5
Леммы о контекстах. Типизируемость подтермов, нетипизируемые предтермы. Лемма подстановки. Теорема о редукции субъекта. Незамкнутость относительно экспансии. Уникальность типов для типизации по Чёрчу. Связь между системами Карри и Черча. Главный (наиболее общий) тип для λ→ в стиле Карри. Свойства подстановки. Унификация. Алгоритм Хиндли-Милнера.
Страница лекции на сайте Computer Science клуба
АвторДенис Москвин
ОрганизаторComputer Science клуб при ПОМИ РАН
Лекции курса
8- Системы типизации лямбда-исчисления. Лекция 1
- Системы типизации лямбда-исчисления. Лекция 2
- Системы типизации лямбда-исчисления. Лекция 3
- Системы типизации лямбда-исчисления. Лекция 4
- Системы типизации лямбда-исчисления. Лекция 5▶ Вы тут
- Системы типизации лямбда-исчисления. Лекция 6
- Системы типизации лямбда-исчисления. Лекция 7
- Системы типизации лямбда-исчисления. Лекция 8
Онлайн-курсы по программированию
3
Машинное обучение для анализа текстов
От бизнес-идеи к ее реализации: учимся инновационному предпринимательству с нуля.
С платными опциями
Разработка игры-платформера на Defold: базовый уровень
Создайте свой первый платформер с нуля! За 7 недель вы не просто освоите движок Defold, а пройдете весь путь геймдев-разработчика: от кода и анимаций до дизайна и сюжета.
Бесплатный
Python для начинающих
Курс посвящен основам программирования на языке Python — одном из самых популярных и понятных языков, идеально подходящих для первого знакомства с IT.
Бесплатный