Types 24

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

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

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

Семинарист: Илья Григорьев aka @ilyagribun.

Ассистент: Яна Ике aka @jijasan.

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

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

Чат курса (Telegram)

Лекции (Zoom)

Семинары (Zoom)

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

classroom для сдачи теоретических домашних заданий

Оценки

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

• Лекция 1, 2 сен 2024. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. Запись.
• Семинар 1, 2 сен 2024. Операционные семантики; Эквивалентности семантик; Preservation и Progress теоремы; Корректность системы типов относительно операционной семантики. Запись.
• Лекция 2, 9 сен 2024. Система типов NatBool+Let. Подстановка. Соглашение об именах. Preservation и progress теоремы. Запись.
• Семинар 2, 9 сен 2024. Семантика с кучей. Эквивалентность семантик с подстановкой и с кучей. Корректность системы типов NatBool+Let. Запись.
• Лекция 3, 16 сен 2024. Нетипизированное лямбда-исчисление. Стратегии редукции. Теорема Чёрча-Россера. Запись.
• Семинар 3, 16 сен 2024. Кодирование Чёрча для типов данных: логические значения, пары, натуральные числа, списки. Комбинатор неподвижной точки. Запись.
• Лекция 4, 23 сен 2024. Просто типизированное лямбда-исчисление. Доказательство слабой нормализуемости. Запись.
• Семинар 4, 23 сен 2024. Теоретико-множественная семантика STLC. Логическая семантика STLC. Пустой тип. Запись.
• Лекция 5, 30 сен 2024. Вычисления с сайд-эффектами: исключения, состояние, I/O. Запись.
• Семинар 5, 30 сен 2024. Изо- и экви- рекурсивные типы данных. Корректность для систем с сайд-эффектами и рекурсией. Запись.
• Лекция 6, 7 окт 2024. Полиморфизм и System F. Лямбда-куб. Запись.
• Семинар 6, 7 окт 2024. Выразительность System F: алгебраические типы данных, Nat. Запись.
• Лекция 7, 14 окт 2024. Система типов Хиндли-Милнера. Декларативные правила вывода. [ Запись].
• Лекция 8, 21 окт 2024. Операторы на типах. Система кайндов. Запись.
• Семинар 7, 21 окт 2024. Унификация. Алгоритмы J и W. Расширения системы Хиндли-Милнера. Запись.
• Лекция 9, 11 ноя 2024. Отношение подтипизации. Решётка типов для STLC. Запись.
• Семинар 8, 11 ноя 2024. Операторы на типах в системе HM. Полиморфная рекурсия. Запись.
• Лекция 10, 18 ноя 2024. Двусторонний вывод типов для STLC с подтипизацией. [ Запись].
• Семинар 9, 18 ноя 2024. Ковариантность и контравариантность. Вывод типов для систем с подтипизацией. [ Запись].
• Лекция 11, 25 ноя 2024. TBA. [ Запись].
• Семинар 11, 25 ноя 2024. TBA. [ Запись].
• Лекция 12, 2 дек 2024. TBA. [ Запись].
• Семинар 12, 2 дек 2024. TBA. [ Запись].
• Лекция 13, 9 дек 2024. TBA. [ Запись].
• Семинар 13, 9 дек 2024. TBA. [ Запись].
• Лекция 14, 16 дек 2024. TBA. [ Запись].
• Семинар 14, 16 дек 2024. TBA. [ Запись].

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

• ТДЗ-1 (теоретическое). Система типов IntBool+Let. Условие. Исходник. Дедлайн: 26 сентября 2024 в 23:59.
• ТДЗ-2 (теоретическое). Тьюринг-полнота нетипизированного лямбда-исчисления. Условие. Исходник. Дедлайн: 3 октября 2024 в 23:59.
• ТДЗ-3 (теоретическое). Алгебраические типы данных и соответствие Карри-Говарда. Условие. Исходник. Дедлайн: 18 октября 2024 в 23:59.
• ПДЗ-1 (практическое). СНИМАЕТСЯ. Оценка за ПДЗ-1 равна максимальной среди оценок за ПДЗ 2-4.
• ПДЗ-2 (практическое). Реализация алгоритма W с различными расширениями. Контест. Дедлайн: 9 декабря в 23:59.
• БТДЗ (бонусное теоретическое). Строковый полиморфизм. Условие. Исходник. Дедлайн: 2 декабря в 23:59.
• ПДЗ-3 (практическое). TBA. [ Условие]. Дедлайн: TBA.
• ПДЗ-4 (практическое). TBA. [ Условие]. Дедлайн: TBA.
• БПДЗ (бонусное практическое). TBA. [ Условие]. Дедлайн: TBA.
• ТДЗ-4 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: TBA.

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

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

Итог = Округление(0.4 * ТДЗ + 0.6 * ПДЗ + Б),

где ТДЗ – средняя оценка за теоретические домашние задания, ПДЗ – за практические, а Б – сумма бонусных баллов, полученных за курс.

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

Литература

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

1. Benjamin C. Pierce, Types and Programming Languages
2. Frank Pfenning, Lecture Notes on Bidirectional Type Checking
3. Jean-Yves Girard, Proofs and Types

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

1. Lectures on the Curry-Howard Isomorphism
2. The Twelf Project
3. Programming Language and Theorem Prover – Lean
4. The Granule Project