Типы данных в языках программирования

Структура курса

1) Простейшие языки: синтаксис, операционная семантика, отношение вычисления, понятие значения.

    Простые типы, отношение типизации. Просто типизированное лямбда-исчисление.

2) Типобезопасность, теоремы о продвижении и сохранении типа.

    Типизация расширений: типы произведений, сумм, конструкция let, рекурсия общего вида.

3) Теорема о сильной нормализации для простых типов. Метод логических отношений.

4) Ссылочные типы, расширение операционной семантики, модель типизированной памяти.

5) Подтипы, отношение вложения для типов. Декларативные и алгоритмические версии отношения подтипизации.  

    Правила вывода, управляемые синтаксисом.

6) Рекурсия на уровне типов. Эквирекурсивные и изорекурсивные типы. Мю-нотация. Катаморфизм и анаморфизм.

7) Полиморфные типы. Переменные типа и подстановки. Реконструкция типов. Let-полиморфизм.

8) Универсальные типы. Система F. Неразрешимость реконструкции, ранги полиморфизма. Параметричность, импредикативность.

    Кодирование стандартных типов в Системе F: булевы значения, числа Черча, списки.

9) Экзистенциальные типы. Понятие пакета (модуля). Абстрактные типы данных. Кодирование экзистенциальных типов в Системе F.

10) Операторы над типами. Отношение присвоения видов (кайндизация). Слабая система с операторами и полная Cистема F-омега.

11) Ограниченная квантификация. Система F с подтипами. Допустимые контексты, ядерное и полное правила вложения. 

      Отношение вложения для контейнерных типов. Уточнение спецификации при типизации стандартных типов данных.

12) Зависимые типы. Типы зависимых произведения и суммы. Зависимые типы первого порядка - система LF. 

       Проблема эквивалентности типов и кайндов для зависимых систем.