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

Бакалавриат 2024/2025

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

Направление: 01.03.02. Прикладная математика и информатика

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

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

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

Формат изучения: без онлайн-курса

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

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

Кредиты: 5

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

Полная версия программы учебной дисциплины

Аннотация

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

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

Умение формализовать системы типов различных языков программирования.

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

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

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

Введение в теорию типов. Система типов и денотационная семантика языка арифметики.
Арифметика с объявлениями. Подстановки и замыкания. Стратегии вычислений.
Операционная семантика лямбда-исчисления. Теорема Чёрча-Россера.
Просто типизированное исчисление. Задача вывода. Алгебраические типы данных.
Вычисления с сайд-эффектами: исключения, состояние, I/O. Изорекурсивные типы данных.
Полиморфизм и System F. Лямбда-куб.
Система типов Хиндли-Милнера. Декларативные правила вывода.
Отношение подтипизации. Решётка типов для STLC.
Двусторонний вывод типов для STLC с подтипизацией.
Введение в теорию категорий. Категорная семантика STLC.
Топосы. Утверждения как типы. Сигма-тип и Пи-тип.
Интерлюдия: линейные типы. Утверждение как ресурс.
Роль равенства в зависимых типах. MLTT и его семантика.
Тема по пожеланиям студентов.

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

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

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

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

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

Авторы

Сысоева Алевтина Александровна
Кононова Елизавета Дмитриевна

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