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

2024/2025

Учебный год

RUS

Обучение ведется на русском языке

5

Кредиты

Кто читает:

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

Статус:

Курс по выбору

Когда читается:

4-й курс, 1, 2 модуль

Преподаватель

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

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

Аннотация

Можно с уверенностью сказать, что сфера разработки языков программирования переживает новый бум — из тех имён, что на слуху, можно назвать 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 * ПДЗ + Б), где ТДЗ – средняя оценка за теоретические домашние задания, ПДЗ – за практические, а Б – сумма бонусных баллов, полученных за курс.

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

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

• Pierce, B. C. (2002). 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=70966

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

• 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

Авторы

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