Types 25

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

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

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

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

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

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

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

Чат курса (Telegram)

Лекции (Zoom)

Семинары (Zoom)

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

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

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

[TBA Оценки]

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

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

• Лекция 1, 16 сен 2025. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [TBA Запись].
• Семинар 1, 19 сен 2025. Small-step и big-step операционная семантика языка NatBool; Эквивалентность семантик; Свойства Preservation и Progress; Здравость системы типов относительно операционной семантики. [TBA Запись].
• Лекция 2, 23 сен 2025. Свойства систем: soundness, completeness и другие; Язык NatBool+Let и операционная семантика с подстановкой; Контекст типизации и здравость системы типов NatBool+Let относительно операционной семантики. [TBA Запись].
• Семинар 2, 23 сен 2025. Семантика с бэгами для NatBool+Let и её эквивалентность семантике с подстановкой; Присваивания и циклы. [TBA Запись].
• Лекция 3, 30 сен 2025. Бета-редукция и подстановка в лямбда-исчислении; Нормальные формы; Альфа- и эта- эквивалентность; Конфлюэнтность лямбда-исчисления. [TBA Запись].
• Семинар 3, 30 сен 2025. Погружение одной системы в другую; Кодирование Чёрча; Нумералы Чёрча; Логические значения, кортежи и списки в лямбда-исчислении; Комбинатор неподвижной точки и его вывод. [TBA Запись].

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

• ТДЗ-1 (теоретическое). TBA. [TBA Условие]. [TBA Исходник]. Дедлайн: 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. Arend Theorem Prover

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

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