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

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

Лучший по критерию «Полезность курса для расширения кругозора и разностороннего развития»

Лучший по критерию «Новизна полученных знаний»

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

Направление: 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).

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

Авторы

Кононова Елизавета Дмитриевна

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