Системы типизации лямбда-исчисления. Лекция 5

Леммы о контекстах. Типизируемость подтермов, нетипизируемые предтермы. Лемма подстановки. Теорема о редукции субъекта. Незамкнутость относительно экспансии. Уникальность типов для типизации по Чёрчу. Связь между системами Карри и Черча. Главный (наиболее общий) тип для λ→ в стиле Карри. Свойства подстановки. Унификация. Алгоритм Хиндли-Милнера.

Страница лекции на сайте Computer Science клуба