Types 23

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

Осенний курс по выбору для студентов 4 курса ПМИ ФКН ВШЭ.

Лектор и семинарист: Павел Соколов aka @TurtlePU.

Полезные ссылки

Канал курса (Telegram)

Чат курса (Telegram)

Основные пары (Zoom)

Дополнительные пары (Zoom)

Записи занятий (Я.Диск)

classroom для сдачи заданий

Оценки

Лекции и семинары

• Лекция 1, 25 сен 2023. Организация курса; Формальные методы и теория типов; Язык IntBool. Запись.
• Семинар 1, 25 сен 2023. Денотационная и операционная семантики; Корректность системы типов языка IntBool. Запись.
• Лекция 2, 25 сен 2023. Preservation и progress теоремы; Лямбда-исчисление и его Тьюринг-полнота. Запись.
• Семинар 2, 2 окт 2023. Операционная семантика лямбда-исчисления; STLC. Запись.
• Лекция 3, 2 окт 2023. Теоретико-множественная семантика STLC; Алгебраические типы данных; Соответствие Карри-Говарда. Запись.
• Семинар 3, 2 окт 2023. Доказательства в интуиционистской логике через CHC; Оператор fix и натуральные числа в STLC. Запись.
• Лекция 4, 9 окт 2023. Оператор явной типизации; типизация параметров в STLC. Полиморфизм и System F; лямбда-куб. Запись.
• Семинар 4, 9 окт 2023. Система типов Хиндли-Милнера, часть 1. Запись.
• Лекция 5, 9 окт 2023. Система типов Хиндли-Милнера, часть 2. Запись.
• Семинар 5, 16 окт 2023. Система типов Хиндли-Милнера и алгебраические типы данных. Полиморфная рекурсия. Запись.
• Лекция 6, 16 окт 2023. Система типов Хиндли-Милнера и отношение подтипизации. Запись.
• Семинар 6, 16 окт 2023. Тип-пересечение и тип-объединение. Задача эквивалентности типов. Двусторонний вывод типов. Запись.

Домашние задания

• ПДЗ-1 (практическое). Реализация программы, обманывающей систему типов одного из мейнстримных языков программирования. 5 баллов за реализацию, 5 баллов за объяснение. Условие. Дедлайн: 7 ноября в 23:59.
• ТДЗ-1 (теоретическое). Решение теоретических задач по темам первой части курса. До 15 баллов. Условие. Исходник. Дедлайн: 23 декабря в 23:59.
• ПДЗ-2 (практическое). Реализация алгоритма W с различными расширениями. Базовая реализация 10 баллов, расширения – до 5 бонусных баллов. Условие. Тестирующая система. Дедлайн: 30 ноября в 23:59.
• ТДЗ-2 (теоретическое). Решение теоретических задач по темам второй части курса. До 15 баллов. Условие. Исходник. Дедлайн: 23 декабря в 23:59.
• ПДЗ-3 (практическое, бонусное). Реализация двусторонней проверки типов. 5 бонусных баллов с весом 0.2 в итоге. Условие. Дедлайн: 23 декабря в 23:59.

Условие теоретических домашних заданий скомпилировано с помощью XeLaTeX.

Правила устной сдачи

Для сдачи теоретического задания доступна также устная сдача. Для того, чтобы сдать задачу устно, нужно:

1. Заранее выписать на лист бумаги или в .pdf все логические правила вывода и термы, необходимые для Вашего решения, а также всё, что должно быть выписано или построено по условию задачи;
2. Договориться со мной (Павлом) о сдаче во время консультаций (пн-пт с 15 до 18 кроме ср) либо сразу до/после занятия;
3. Рассказать решение, опираясь на Ваши выкладки.

Итоговая оценка за курс

Итог = Округление(0.1 * ПДЗ-1 + 0.2 * ПДЗ-2 + 0.2 * ПДЗ-3 + 0.25 * ТДЗ-1 + 0.25 * ТДЗ-2).

Округление арифметическое.

Литература

Основная литература

1. Benjamin C. Pierce, Types and Programming Languages
2. Frank Pfenning, Lecture Notes on Bidirectional Type Checking

Дополнительная литература

1. Lectures on the Curry-Howard Isomorphism