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

Современные функциональные языки программирования, такие как Haskell, наследники ML (SML, Ocaml, F#), Agda2 и т.п., обладают весьма богатыми и сложными системами типов. Несмотря на такое разнообразие, эти системы имеют в своей основе хорошо проработанную формальную теорию типизированных лямбда-исчислений.

В рамках курса рассматриваются различные системы типизации лямбда-исчисления. Понятие типа вводится на примере просто типизированного чистого лямбда-исчисления. Исследуются два основных подхода к типизации лямбда-исчисления: в стиле Карри и в стиле Чёрча. Обсуждаются следующие системы: полиморфные типы (System F), операторы над типами, полиморфизм высших порядков, зависимые типы, рекурсивные типы. Для изучаемых систем исследуются проблемы проверки, присваивания (синтеза) и населенности типов. Обсуждается связь между различными логическими системами и системами типов.