Бакалавриат
2023/2024![Планируемые результаты обучения](/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. Прикладная математика и информатика
Где читается:
Факультет компьютерных наук
Когда читается:
3-й курс, 1, 2 модуль
Формат изучения:
без онлайн-курса
Охват аудитории:
для своего кампуса
Преподаватели:
Соколов Павел Павлович
Язык:
русский
Кредиты:
5
Контактные часы:
56
Программа дисциплины
Аннотация
Можно с уверенностью сказать, что сфера разработки языков программирования переживает новый бум — из тех имён, что на слуху, можно назвать Rust, Julia, Kotlin, Crystal, Zig,.. Причём основным selling point большинства новых языков является какая-то инновационная система типов. Данный курс как раз и посвящен введению в теорию типов — учение о дизайне систем типов и разработке соответствующих алгоритмов. Будем решать как теоретические, так и практические задачи; если вам до этого нравились курсы по дискретной математике, логике, вычислимости и алгоритмам, вам понравится и здесь.
Планируемые результаты обучения
- Знакомство с теорией типов.
- Умение формализовать системы типов различных языков программирования.
- Изучение основных алгоритмов проверки и вывода типов.
- Знакомство с взаимосвязями между теорией типов и логикой, написанием кода и доказательством теорем.
Содержание учебной дисциплины
- Введение в теорию типов. Система типов и денотационная семантика языка арифметики.
- Корректность, preservation и progress. Лямбда-исчисление и его Тьюринг-полнота.
- Теоретико-множественная семантика STLC. Алгебраические типы данных. Соответствие Карри-Говарда.
- Оператор явной типизации. Типизация параметров в STLC. Полиморфизм и System F. Лямбда-куб.
- Синтаксическая система типизации по Хиндли-Милнеру. Алгоритм W.
- Система типов Хиндли-Милнера и отношение подтипизации.
- Полиморфизм и подтипизация. Ко- и контравариантность.
- Рекурсивные типы.
- Рекурсивные типы и полиморфизм. Индуктивные типы.
- Операторы на типах. Система кайндов.
- Тайпклассы, трейты и функторы.
- Простые зависимые типы. Сигма-тип и Пи-тип.
- W-типы. Индукция. Язык Twelf.
- Равенство в DTT. Система типов Мартина-Лёфа.
Элементы контроля
- Практическое домашнее задание 1Реализация программы, обманывающей систему типов одного из мейнстримных языков программирования. 5 баллов за реализацию, 5 баллов за объяснение.
- Теоретическое домашнее задание 1Решение теоретических задач по темам первой части курса. До 15 баллов.
- Практическое домашнее задание 2Реализация алгоритма W с различными расширениями. Базовая реализация 10б, расширения – до 5 бб.
- Теоретическое домашнее задание 2Решение теоретических задач по темам второй части курса. До 15 баллов.
- Практическое домашнее задание 3Реализация двусторонней проверки типов с различными расширениями. Три вариации до 5 баллов за каждую.
Промежуточная аттестация
- 2023/2024 2nd moduleИтог = Округление(0.1 * ПДЗ1 + 0.2 * ПДЗ2 + 0.2 * ПДЗ3 + 0.25 * ТДЗ1 + 0.25 * ТДЗ2).
Список литературы
Рекомендуемая основная литература
- 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