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

Магистратура 2026/2027

Статус: Курс по выбору (Современные компьютерные науки)

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

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

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

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

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

Кредиты: 6

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

Дополнительные материалы в LMS Задать вопрос

Аннотация

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

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

Сформировать комплексное понимание теории типов и её практического применения: от формализации систем типов в языках программирования до реализации алгоритмов проверки и вывода типов, а также освоения связей между теорией типов, логикой и доказательством теорем в контексте написания кода.

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

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

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

Введение в теорию типов. Система типов и денотационная семантика языка арифметики.
Арифметика с объявлениями. Подстановки и замыкания. Preservation и progress теоремы.
Лямбда-исчисление: определение, операционная семантика, конфлюэнтность.
Алгебраические типы данных и тип функций.
Категорная семантика. Операторы на типах.
Полиморфизм и System F. Параметричность. Лямбда-куб.
Система типов Хиндли-Милнера. Декларативные правила вывода.
Отношение подтипизации. Ко- и контравариантность.
Логическое программирование, классы типов и их взаимосвязь.
Рекурсивные типы данных и их денотационная семантика.
Программа как доказательство. Пруверы. Зависимые типы.
Полиморфизм в DTT. Парадокс Жирара. Вселенные.
Роль равенства в зависимых типах. Гомотопическая теория типов.
Субструктурные логики и системы типов. Утверждения как сессии.
Тема по пожеланиям студентов.

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

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

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

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

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

Авторы

Емашева Валерия Анатольевна

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