Бакалавриат 2026/2027

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

Статус: Курс по выбору (Прикладная математика и информатика)

Кто читает: Департамент больших данных и информационного поиска

Где читается: Факультет компьютерных наук

Когда читается: 4-й курс, 1, 2 модуль

Охват аудитории: для своего кампуса

Язык: русский

Кредиты: 5

Контактные часы: 56

Программа дисциплины

Аннотация

Можно с уверенностью сказать, что сфера разработки языков программирования переживает новый бум — из тех имён, что на слуху, можно назвать Rust, Zig, Lean, Julia, Kotlin,.. Причём основным selling point большинства новых языков является какая-то инновационная система типов. Данный курс как раз и посвящен введению в теорию типов — учение о дизайне систем типов и разработке соответствующих алгоритмов. Будем решать как теоретические, так и практические задачи; если вам до этого нравились курсы по дискретной математике, логике, вычислимости и алгоритмам, вам понравится и здесь.

Цель освоения дисциплины

• знакомство с взаимосвязями между теорией типов и логикой, написанием кода и доказательством теорем

Планируемые результаты обучения

• Знакомство с теорией типов.
• Умение формализовать системы типов различных языков программирования.
• Изучение основных алгоритмов проверки и вывода типов.
• Знакомство с взаимосвязями между теорией типов и логикой, написанием кода и доказательством теорем.

Содержание учебной дисциплины

• Язык NatBool+Let и его денотационная семантика. Типы как носители смысла.
• NatBool+Fun и его строгая нормализация.
• Неподвижная точка. Операторы на типах.
• Изорекурсивные типы данных.
• Лямбда-исчисление и тезис Чёрча-Тьюринга.
• Полиморфизм и System F. Параметричность.
• Подтипизация. Ко- и контравариантность.
• Классы типов и логика первого порядка.
• Лямбда-куб. Исчисление конструкций.
• Индуктивные типы. Парадокс Жирара.
• Двусторонний вывод типов.
• Доказательство нормализации MLTT.
• Группоидная модель MLTT. UIP и UA.
• Кубическая теория типов: интервал, Glue.
• (Higher) observational type theory.

Элементы контроля

• Теоретическое домашнее задание 1
  Формулировка и доказательство здравости для системы IntBool с объявлениями.
• Теоретическое домашнее задание 2
  Доказательство несложных утверждений в STLC.
• Практическое домашнее задание 1
  Реализация парсера и форматировщика учебного языка программирования.
• Теоретическое домашнее задание 3
  Доказательство Тьюринг-полноты нетипизированного лямбда-исчисления.
• Практическое домашнее задание 2
  Реализация алгоритма W с различными расширениями. Базовая реализация 10б, расширения – до 0.25 бонусных баллов.
• Бонусное теоретическое домашнее задание
  Исследование свойств системы типов со строковым полиморфизмом. До 0.5 бонусных баллов.
• Практическое домашнее задание 3
  Реализация алгоритма вывода инстансов. Базовая реализация 10б, расширения – до 0.25 бонусных баллов.
• Бонусное практическое домашнее задание
  Доказательство (с устной защитой) коммутативности сложения в Twelf. До 0.5 бонусных баллов.
• Теоретическое домашнее задание 4
  Доказательство утверждений в Agda.
• Практическое домашнее задание 4
  Реализация двусторонней проверки типов с различными расширениями. Также можно получить до 0.25 бб.
• Экзамен

Промежуточная аттестация

• 2026/2027 2nd module
  Итог = Округление(0.4 * ТДЗ + 0.4 * ПДЗ + 0.2 * Э + Б), где ТДЗ – средняя оценка за теоретические домашние задания, ПДЗ – за практические, Э – оценка за экзамен, а Б – сумма полученных за курс бонусов.

Список литературы

Рекомендуемая основная литература

• Pierce, B. C. (2005). Advanced Topics in Types and Programming Languages. Cambridge, Mass: The MIT Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=138471

Рекомендуемая дополнительная литература

• Sørensen, M. H., & Urzyczyn, P. (2006). Lectures on the Curry-Howard Isomorphism (Vol. 1st ed). Amsterdam: Elsevier Science. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=196231

Авторы

• Соколов Павел Павлович