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

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
(→‎Лекции и семинары)
(→‎Лекции и семинары)
Строка 32: Строка 32:
  
 
* '''Лекция 1, 16 сен 2025'''. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [https://disk.yandex.ru/d/mzXlT0U3MzEZkQ/%D0%9F%D0%9C%D0%98/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F%202025-09-16T11-38-59Z.mp4 Запись].
 
* '''Лекция 1, 16 сен 2025'''. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [https://disk.yandex.ru/d/mzXlT0U3MzEZkQ/%D0%9F%D0%9C%D0%98/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F%202025-09-16T11-38-59Z.mp4 Запись].
−
* '''Семинар 1, 19 сен 2025'''. Small-step и big-step операционная семантика языка NatBool; Эквивалентность семантик; Свойства Preservation и Progress; Здравость системы типов относительно операционной семантики. [https://miro.com/app/board/uXjVJFr_x58=/?share_link_id=820988334992 конспект] [https://disk.yandex.ru/d/VR048aIKOHNuGA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80/%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D1%8C%D0%B5%D0%B2%202025-09-19T11-44-17Z.mp4 Запись].
+
* '''Семинар 1, 19 сен 2025'''. Small-step и big-step операционная семантика языка NatBool; Эквивалентность семантик; Свойства Preservation и Progress; Здравость системы типов относительно операционной семантики. [https://miro.com/app/board/uXjVJFr_x58=/?share_link_id=820988334992 Конспект]. [https://disk.yandex.ru/d/VR048aIKOHNuGA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80/%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D1%8C%D0%B5%D0%B2%202025-09-19T11-44-17Z.mp4 Запись].
 
* '''Лекция 2, 23 сен 2025'''. Свойства систем: soundness, completeness и другие; Язык NatBool+Let и операционная семантика с подстановкой; Контекст типизации и здравость системы типов NatBool+Let относительно операционной семантики. [https://disk.yandex.ru/d/VR048aIKOHNuGA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202025-09-23T11-39-24Z.mp4 Запись].
 
* '''Лекция 2, 23 сен 2025'''. Свойства систем: soundness, completeness и другие; Язык NatBool+Let и операционная семантика с подстановкой; Контекст типизации и здравость системы типов NatBool+Let относительно операционной семантики. [https://disk.yandex.ru/d/VR048aIKOHNuGA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202025-09-23T11-39-24Z.mp4 Запись].
 
* '''Семинар 2, 23 сен 2025'''. Семантика с бэгами для NatBool+Let и её эквивалентность семантике с подстановкой; Присваивания и циклы. [https://disk.yandex.ru/d/VR048aIKOHNuGA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80/%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D1%8C%D0%B5%D0%B2%202025-09-23T15-06-40Z.mp4 Запись].
 
* '''Семинар 2, 23 сен 2025'''. Семантика с бэгами для NatBool+Let и её эквивалентность семантике с подстановкой; Присваивания и циклы. [https://disk.yandex.ru/d/VR048aIKOHNuGA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80/%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D1%8C%D0%B5%D0%B2%202025-09-23T15-06-40Z.mp4 Запись].
−
* '''Лекция 3, 30 сен 2025'''. Бета-редукция и подстановка в лямбда-исчислении; Нормальные формы; Альфа- и эта- эквивалентность; Конфлюэнтность лямбда-исчисления. [https://miro.com/app/board/uXjVJBffPT4=/?share_link_id=807334183872 Конспект] [https://disk.yandex.ru/d/VR048aIKOHNuGA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202025-09-30T11-49-15Z.mp4 Запись].
+
* '''Лекция 3, 30 сен 2025'''. Бета-редукция и подстановка в лямбда-исчислении; Нормальные формы; Альфа- и эта- эквивалентность; Конфлюэнтность лямбда-исчисления. [https://miro.com/app/board/uXjVJBffPT4=/?share_link_id=807334183872 Конспект]. [https://disk.yandex.ru/d/VR048aIKOHNuGA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202025-09-30T11-49-15Z.mp4 Запись].
 
* '''Семинар 3, 30 сен 2025'''. Погружение одной системы в другую; Кодирование Чёрча; Нумералы Чёрча; Логические значения, кортежи и списки в лямбда-исчислении; Комбинатор неподвижной точки и его вывод. [https://disk.yandex.ru/d/VR048aIKOHNuGA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80/%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D1%8C%D0%B5%D0%B2%202025-09-30T15-02-19Z.mp4 Запись].
 
* '''Семинар 3, 30 сен 2025'''. Погружение одной системы в другую; Кодирование Чёрча; Нумералы Чёрча; Логические значения, кортежи и списки в лямбда-исчислении; Комбинатор неподвижной точки и его вывод. [https://disk.yandex.ru/d/VR048aIKOHNuGA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80/%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D1%8C%D0%B5%D0%B2%202025-09-30T15-02-19Z.mp4 Запись].
−
* '''Семинар 4, 7 окт 2025''' (online). Просто типизированное лямбда-исчисление; Тип-произведение и тип-сумма; Теоретико-множественная семантика просто типизированного исчисления. [TBA Конспект] [https://disk.yandex.ru/d/mzXlT0U3MzEZkQ/%D0%9F%D0%9C%D0%98/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80/%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D1%8C%D0%B5%D0%B2%202025-10-07T15-04-11Z.mp4 Запись].
+
* '''Семинар 4, 7 окт 2025''' (online). Просто типизированное лямбда-исчисление; Тип-произведение и тип-сумма; Теоретико-множественная семантика просто типизированного исчисления. [TBA Конспект]. [https://disk.yandex.ru/d/mzXlT0U3MzEZkQ/%D0%9F%D0%9C%D0%98/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80/%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D1%8C%D0%B5%D0%B2%202025-10-07T15-04-11Z.mp4 Запись].
−
* '''Лекция 4, 10 окт 2025''' (online). Сильная нормализация STLC с произведениями; Теоретико-множественная и логическая семантики типизированного исчисления. [https://miro.com/app/board/uXjVJ8Yg69A=/?share_link_id=341389485655 Конспект] Запись доступна в чате в Telegram.
+
* '''Лекция 4, 10 окт 2025''' (online). Сильная нормализация STLC с произведениями; Теоретико-множественная и логическая семантики типизированного исчисления. [https://miro.com/app/board/uXjVJ8Yg69A=/?share_link_id=341389485655 Конспект]. Запись доступна в чате в Telegram.
 
* '''Лекция 5, 14 окт 2025'''. Теоретико-категорная семантика STLC с произведениями. [TBA Запись].
 
* '''Лекция 5, 14 окт 2025'''. Теоретико-категорная семантика STLC с произведениями. [TBA Запись].
−
* '''Семинар 5, 14 окт 2025''' (online). Решение задач на теорию категорий. [TBA Конспект] [TBA Запись].
+
* '''Семинар 5, 14 окт 2025''' (online). Решение задач на теорию категорий. [TBA Конспект]. [TBA Запись].
−
* '''Лекция 6, 20 окт 2025''' (online). Функторы и операторы на типах. [https://miro.com/app/board/uXjVJ31dIpw=/?share_link_id=136783004017 Конспект] Запись доступна в чате в Telegram.
+
* '''Лекция 6, 20 окт 2025''' (online). Функторы и операторы на типах. [https://miro.com/app/board/uXjVJ31dIpw=/?share_link_id=136783004017 Конспект]. Запись доступна в чате в Telegram.
−
* '''Семинар 6, 21 окт 2025''' (online). Парсеры; Рекурсия; Сайд-эффекты. [TBA Конспект] [TBA Запись].
+
* '''Семинар 6, 21 окт 2025''' (online). Парсеры; Рекурсия; Сайд-эффекты. [TBA Конспект]. [TBA Запись].
−
* '''Лекция 7, 21 окт 2025'''. Полиморфизм; Система F; Параметричность. [https://miro.com/app/board/uXjVJ2iK9V0=/?share_link_id=770454466357 Конспект] [TBA Запись].
+
* '''Лекция 7, 21 окт 2025'''. Полиморфизм; Система F; Параметричность. [https://miro.com/app/board/uXjVJ2iK9V0=/?share_link_id=770454466357 Конспект]. [TBA Запись].
−
* '''Семинар 7, 21 окт 2025''' (online). О выразительности системы F; Задача вывода типов. [TBA Конспект] [https://disk.yandex.ru/d/mzXlT0U3MzEZkQ/%D0%9F%D0%9C%D0%98/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80/%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D1%8C%D0%B5%D0%B2%202025-10-21T15-07-22Z.mp4 Запись].
+
* '''Семинар 7, 21 окт 2025''' (online). О выразительности системы F; Задача вывода типов. [TBA Конспект]. [https://disk.yandex.ru/d/mzXlT0U3MzEZkQ/%D0%9F%D0%9C%D0%98/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80/%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D1%8C%D0%B5%D0%B2%202025-10-21T15-07-22Z.mp4 Запись].
−
* '''Лекция 8, 3 ноя 2025''' (online). TBA. [TBA Конспект] [TBA Запись].
+
* '''Лекция 8, 3 ноя 2025''' (online). TBA. [TBA Конспект]. [TBA Запись].
−
* '''Семинар 8, 11 ноя 2025''' (online). TBA. [TBA Конспект] [TBA Запись]
+
* '''Семинар 8, 11 ноя 2025''' (online). TBA. [TBA Конспект]. [TBA Запись]
−
* '''Лекция 9, 11 ноя 2025'''. TBA. [TBA Конспект] [TBA Запись].
+
* '''Лекция 9, 11 ноя 2025'''. TBA. [TBA Конспект]. [TBA Запись].
−
* '''Семинар 9, 11 ноя 2025''' (online). TBA. [TBA Конспект] [TBA Запись].
+
* '''Семинар 9, 11 ноя 2025''' (online). TBA. [TBA Конспект]. [TBA Запись].
  
 
== Домашние задания ==
 
== Домашние задания ==

Версия 18:44, 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 Конспект]. Запись.
  • Лекция 4, 10 окт 2025 (online). Сильная нормализация STLC с произведениями; Теоретико-множественная и логическая семантики типизированного исчисления. Конспект. Запись доступна в чате в Telegram.
  • Лекция 5, 14 окт 2025. Теоретико-категорная семантика STLC с произведениями. [TBA Запись].
  • Семинар 5, 14 окт 2025 (online). Решение задач на теорию категорий. [TBA Конспект]. [TBA Запись].
  • Лекция 6, 20 окт 2025 (online). Функторы и операторы на типах. Конспект. Запись доступна в чате в Telegram.
  • Семинар 6, 21 окт 2025 (online). Парсеры; Рекурсия; Сайд-эффекты. [TBA Конспект]. [TBA Запись].
  • Лекция 7, 21 окт 2025. Полиморфизм; Система F; Параметричность. Конспект. [TBA Запись].
  • Семинар 7, 21 окт 2025 (online). О выразительности системы F; Задача вывода типов. [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 (теоретическое). 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=93251»