Types 25

Материал из Wiki - Факультет компьютерных наук
Версия от 19:15, 18 ноября 2025; TurtlePU (обсуждение | вклад)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Перейти к: навигация, поиск

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

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

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

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

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

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

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

Чат курса (Telegram)

Лекции (Zoom)

Семинары (Zoom)

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

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

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). Просто типизированное лямбда-исчисление; Тип-произведение и тип-сумма; Теоретико-множественная семантика просто типизированного исчисления. Конспект. Запись.
  • Лекция 4, 10 окт 2025 (online). Сильная нормализация STLC с произведениями; Теоретико-множественная и логическая семантики типизированного исчисления. Конспект. Запись (доступна участникам чата в Telegram).
  • Лекция 5, 14 окт 2025. Теоретико-категорная семантика STLC с произведениями. [TBA Запись].
  • Семинар 5, 14 окт 2025 (online). Решение задач на теорию категорий. Конспект. [TBA Запись].
  • Лекция 6, 20 окт 2025 (online). Функторы и операторы на типах. Конспект. Запись (доступна участникам чата в Telegram).
  • Семинар 6, 21 окт 2025 (online). Парсеры; Рекурсия; Сайд-эффекты. Конспект. [TBA Запись].
  • Лекция 7, 21 окт 2025. Полиморфизм; Система F; Параметричность. Конспект. [TBA Запись].
  • Семинар 7, 21 окт 2025 (online). О выразительности системы F; Задача вывода типов. Конспект. Запись.
  • Лекция 8, 3 ноя 2025 (online). Лямбда-куб. Система типов Хиндли-Милнера: декларативные правила вывода. Конспект. [TBA Запись].
  • Семинар 8, 11 ноя 2025 (online). Алгоритмы W и J для системы типов Хиндли-Милнера; задача унификации. [TBA Конспект]. [TBA Запись]
  • Лекция 9, 11 ноя 2025. Отношение подтипизации в STLC и Системе Fw; Ковариантность и контравариантность. Конспект. [TBA Запись].
  • Семинар 9, 11 ноя 2025 (online). Алгоритмы G и G Atomic для унификации в системе с подтипизацией. [TBA Конспект]. [TBA Запись].
  • Лекция 10, 18 ноя 2025 (online). Ad-hoc полиморфизм; Алгоритм instance resolution; Логика предикатов и её связь с классами типов; Логическое программирование. Конспект. [TBA Запись].
  • Семинар 10, 18 ноя 2025 (online). TBA. [TBA Конспект]. [TBA Запись].
  • Лекция 11, 25 ноя 2025. TBA. [TBA Конспект]. [TBA Запись].
  • Семинар 11, 25 ноя 2025 (online). TBA. [TBA Конспект]. [TBA Запись].
  • Лекция 12, 2 дек 2025. TBA. [TBA Конспект]. [TBA Запись].
  • Семинар 12, 2 дек 2025 (online). TBA. [TBA Конспект]. [TBA Запись].
  • Лекция 13, 9 дек 2025. TBA. [TBA Конспект]. [TBA Запись].
  • Семинар 13, 9 дек 2025 (online). TBA. [TBA Конспект]. [TBA Запись].
  • Лекция 14, 16 дек 2025. TBA. [TBA Конспект]. [TBA Запись].
  • Семинар 14, 16 дек 2025 (online). TBA. [TBA Конспект]. [TBA Запись].

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

  • ТДЗ-1 (теоретическое). Система IntBool+Let. Условие. Исходник. Дедлайн: 7 октября в 18:10.
  • ТДЗ-2 (теоретическое). Тьюринг-полнота лямбда-исчисления. Условие. Исходник. Дедлайн: 16 октября в 18:10.
  • ТДЗ-3 (теоретическое). STLC как система доказательств. Условие. Исходник. Дедлайн: 5 ноября в 18:10.
  • ДЗ-4. 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
Источник — «http://wiki.cs.hse.ru/index.php?title=Types_25&oldid=93731»