Бакалавриат
2024/2025![Планируемые результаты обучения](/f/src/global/i/edu/results.svg)
![Содержание учебной дисциплины](/f/src/global/i/edu/sections.svg)
![Элементы контроля](/f/src/global/i/edu/controls.svg)
![Промежуточная аттестация](/f/src/global/i/edu/intermediate_certification.svg)
![Список литературы](/f/src/global/i/edu/library.svg)
Типы в языках программирования
Статус:
Курс по выбору (Прикладная математика и информатика)
Направление:
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 * ПДЗ + Б), где ТДЗ – средняя оценка за теоретические домашние задания, ПДЗ – за практические, а Б – сумма бонусных баллов, полученных за курс.
Список литературы
Рекомендуемая основная литература
- 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