Types 25 — различия между версиями

Версия 18:13, 22 октября 2025

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

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

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

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

Ассистент: Ислам Талипов aka @lishy2.

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

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

Чат курса (Telegram)

Лекции (Zoom)

Семинары (Zoom)

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

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

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

[TBA Оценки]

Программа учебной дисциплины

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

• Лекция 1, 16 сен 2025. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. Запись.
• Семинар 1, 19 сен 2025. Small-step и big-step операционная семантика языка NatBool; Эквивалентность семантик; Свойства Preservation и Progress; Здравость системы типов относительно операционной семантики. конспект Запись.
• Лекция 2, 23 сен 2025. Свойства систем: soundness, completeness и другие; Язык NatBool+Let и операционная семантика с подстановкой; Контекст типизации и здравость системы типов NatBool+Let относительно операционной семантики. Запись.
• Семинар 2, 23 сен 2025. Семантика с бэгами для NatBool+Let и её эквивалентность семантике с подстановкой; Присваивания и циклы. Запись.
• Лекция 3, 30 сен 2025. Бета-редукция и подстановка в лямбда-исчислении; Нормальные формы; Альфа- и эта- эквивалентность; Конфлюэнтность лямбда-исчисления. Конспект Запись.
• Семинар 3, 30 сен 2025. Погружение одной системы в другую; Кодирование Чёрча; Нумералы Чёрча; Логические значения, кортежи и списки в лямбда-исчислении; Комбинатор неподвижной точки и его вывод. Запись.
• Семинар 4, 7 окт 2025 (online). Просто типизированное лямбда-исчисление; Тип-произведение и тип-сумма; Теоретико-множественная семантика просто типизированного исчисления. [TBA Конспект] [TBA Запись].
• Лекция 4, 10 окт 2025 (online). Сильная нормализация STLC с произведениями; Теоретико-множественная и логическая семантики типизированного исчисления. Конспект Запись доступна в чате в Telegram.
• Лекция 5, 14 окт 2025. Теоретико-категорная семантика STLC с произведениями. [TBA Запись].
• Семинар 5, 14 окт 2025 (online). Решение задач на теорию категорий. [TBA Конспект] [TBA Запись].
• Лекция 6, 20 окт 2025 (online). Функторы и операторы на типах. [TBA Конспект] Запись доступна в чате в Telegram.
• Семинар 6, 21 окт 2025 (online). Парсеры; Рекурсия; Сайд-эффекты. [TBA Конспект] [TBA Запись].
• Лекция 7, 21 окт 2025. Полиморфизм; Система F; Параметричность. [TBA Конспект] [TBA Запись].
• Семинар 7, 21 окт 2025 (online). О выразительности системы F; Задача вывода типов. [TBA Конспект] [TBA Запись].
• Лекция 8, 3 ноя 2025 (online). TBA. [TBA Конспект] [TBA Запись].
• Семинар 8, 11 ноя 2025 (online). TBA. [TBA Конспект] [TBA Запись]
• Лекция 9, 11 ноя 2025. TBA. [TBA Конспект] [TBA Запись].
• Семинар 9, 11 ноя 2025 (online). TBA. [TBA Конспект] [TBA Запись].

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

• ТДЗ-1 (теоретическое). Система IntBool+Let. Условие. Исходник. Дедлайн: 7 октября в 18:10.
• ТДЗ-2 (теоретическое). Тьюринг-полнота лямбда-исчисления. Условие. Исходник. Дедлайн: 16 октября в 18:10.
• ДЗ-3. TBA.

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

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

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

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

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

Автоматы за экзамен TBA.

Литература

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

1. Benjamin C. Pierce, Types and Programming Languages
2. Frank Pfenning, Lecture Notes on Bidirectional Type Checking
3. Jean-Yves Girard, Proofs and Types
4. Philip Wadler, Wen Kokke, Jeremy G. Siek, Programming Language Foundations in Agda

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

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