Types 25 — различия между версиями
Материал из Wiki - Факультет компьютерных наук
TurtlePU (обсуждение | вклад) (→Основная литература) |
TurtlePU (обсуждение | вклад) (→Лекции и семинары) |
||
| (не показаны 22 промежуточные версии этого же участника) | |||
| Строка 19: | Строка 19: | ||
[https://us06web.zoom.us/j/83929037513?pwd=BcJ3cG7YuSBkrxxuDrjOQcVxtm4xEM.1 Семинары (Zoom)] | [https://us06web.zoom.us/j/83929037513?pwd=BcJ3cG7YuSBkrxxuDrjOQcVxtm4xEM.1 Семинары (Zoom)] | ||
| − | [ | + | [https://disk.yandex.ru/d/VR048aIKOHNuGA Записи занятий (Я.Диск)] |
[https://classroom.google.com/c/ODA2NDcxMTk1Mzgz?cjc=y32mapjm classroom для сдачи теоретических домашних заданий] | [https://classroom.google.com/c/ODA2NDcxMTk1Mzgz?cjc=y32mapjm classroom для сдачи теоретических домашних заданий] | ||
| − | [ | + | [https://classroom.github.com/classrooms/232351245-types-hse-2025 classroom для сдачи практических домашних заданий] |
[TBA Оценки] | [TBA Оценки] | ||
| Строка 31: | Строка 31: | ||
== Лекции и семинары == | == Лекции и семинары == | ||
| − | * '''Лекция 1, 16 сен 2025'''. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [ | + | * '''Лекция 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; Здравость системы типов относительно операционной семантики. [ | + | * '''Семинар 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 относительно операционной семантики. [ | + | * '''Лекция 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 и её эквивалентность семантике с подстановкой; Присваивания и циклы. [ | + | * '''Семинар 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 Конспект] [ | + | * '''Лекция 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'''. Погружение одной системы в другую; Кодирование Чёрча; Нумералы Чёрча; Логические значения, кортежи и списки в лямбда-исчислении; Комбинатор неподвижной точки и его вывод. [ | + | * '''Семинар 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). Просто типизированное лямбда-исчисление; Тип-произведение и тип-сумма; Теоретико-множественная семантика просто типизированного исчисления. [https://miro.com/app/board/uXjVJ905vI8=/?share_link_id=694305623690 Конспект]. [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 Конспект]. [https://t.me/c/1630403967/678 Запись] (доступна участникам чата в Telegram). |
| + | * '''Лекция 5, 14 окт 2025'''. Теоретико-категорная семантика STLC с произведениями. [TBA Запись]. | ||
| + | * '''Семинар 5, 14 окт 2025''' (online). Решение задач на теорию категорий. [https://miro.com/app/board/uXjVJ6N01Q8=/?share_link_id=609779984354 Конспект]. [TBA Запись]. | ||
| + | * '''Лекция 6, 20 окт 2025''' (online). Функторы и операторы на типах. [https://miro.com/app/board/uXjVJ31dIpw=/?share_link_id=136783004017 Конспект]. [https://t.me/c/1630403967/720 Запись] (доступна участникам чата в Telegram). | ||
| + | * '''Семинар 6, 21 окт 2025''' (online). Парсеры; Рекурсия; Сайд-эффекты. [https://miro.com/app/board/uXjVJ3brZyw=/?share_link_id=694748358404 Конспект]. [TBA Запись]. | ||
| + | * '''Лекция 7, 21 окт 2025'''. Полиморфизм; Система F; Параметричность. [https://miro.com/app/board/uXjVJ2iK9V0=/?share_link_id=770454466357 Конспект]. [TBA Запись]. | ||
| + | * '''Семинар 7, 21 окт 2025''' (online). О выразительности системы F; Задача вывода типов. [https://miro.com/app/board/uXjVJ2oG-gc=/?share_link_id=82972642906 Конспект]. [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). Лямбда-куб. Система типов Хиндли-Милнера: декларативные правила вывода. [https://miro.com/app/board/uXjVJwlOfzg=/?share_link_id=308731505730 Конспект]. [TBA Запись]. | ||
| + | * '''Семинар 8, 11 ноя 2025''' (online). Алгоритмы W и J для системы типов Хиндли-Милнера; задача унификации. [TBA Конспект]. [TBA Запись] | ||
| + | * '''Лекция 9, 11 ноя 2025'''. Отношение подтипизации в STLC и Системе Fw; Ковариантность и контравариантность. [https://miro.com/app/board/uXjVJs6c66k=/?share_link_id=906680708688 Конспект]. [TBA Запись]. | ||
| + | * '''Семинар 9, 11 ноя 2025''' (online). Алгоритмы G и G Atomic для унификации в системе с подтипизацией. [TBA Конспект]. [TBA Запись]. | ||
| + | * '''Лекция 10, 18 ноя 2025''' (online). Ad-hoc полиморфизм; Алгоритм instance resolution; Логика предикатов и её связь с классами типов; Логическое программирование. [https://miro.com/app/board/uXjVJohCSCI=/?share_link_id=207335723512 Конспект]. [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 Запись]. | ||
== Домашние задания == | == Домашние задания == | ||
| Строка 44: | Строка 64: | ||
* ТДЗ-1 (теоретическое). Система IntBool+Let. [https://drive.google.com/file/d/1SJKjInFn_r4Rbcs51LdvANlhsH524nCs/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1E8nmyrK9AJ-9aXsIiekvOJH6lCIQUOXQ/view?usp=drive_link Исходник]. Дедлайн: '''7 октября в 18:10'''. | * ТДЗ-1 (теоретическое). Система IntBool+Let. [https://drive.google.com/file/d/1SJKjInFn_r4Rbcs51LdvANlhsH524nCs/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1E8nmyrK9AJ-9aXsIiekvOJH6lCIQUOXQ/view?usp=drive_link Исходник]. Дедлайн: '''7 октября в 18:10'''. | ||
* ТДЗ-2 (теоретическое). Тьюринг-полнота лямбда-исчисления. [https://drive.google.com/file/d/1tjrkIMUgvjVvl3tLZN9z1knObxPTg83z/view?usp=drive_link Условие]. [https://drive.google.com/file/d/149eC5LqeZuePpAzKdOdCgWSPTRjnSV1c/view?usp=drive_link Исходник]. Дедлайн: '''16 октября в 18:10'''. | * ТДЗ-2 (теоретическое). Тьюринг-полнота лямбда-исчисления. [https://drive.google.com/file/d/1tjrkIMUgvjVvl3tLZN9z1knObxPTg83z/view?usp=drive_link Условие]. [https://drive.google.com/file/d/149eC5LqeZuePpAzKdOdCgWSPTRjnSV1c/view?usp=drive_link Исходник]. Дедлайн: '''16 октября в 18:10'''. | ||
| − | * | + | * ТДЗ-3 (теоретическое). STLC как система доказательств. [https://drive.google.com/file/d/1Lo97PitL3eEbxd4ZLeqIB7n69YfI6shg/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1N_QcG4I72zL0bnZ4IXBChNfzjeApAwUZ/view?usp=drive_link Исходник]. Дедлайн: '''5 ноября в 18:10'''. |
| + | * ДЗ-4. TBA. | ||
Условие теоретических домашних заданий скомпилировано с помощью pdfLaTeX. | Условие теоретических домашних заданий скомпилировано с помощью pdfLaTeX. | ||
| Строка 64: | Строка 85: | ||
# [http://prog.tversu.ru/library/tapl.pdf Benjamin C. Pierce, Types and Programming Languages] | # [http://prog.tversu.ru/library/tapl.pdf Benjamin C. Pierce, Types and Programming Languages] | ||
# [https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bidirectional.pdf Frank Pfenning, Lecture Notes on Bidirectional Type Checking] | # [https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bidirectional.pdf Frank Pfenning, Lecture Notes on Bidirectional Type Checking] | ||
| − | # Jean-Yves Girard, Proofs and Types | + | # [https://drive.google.com/file/d/1diURe89Dv3Wu9Bryy4b1CtJ-SWnLMowS/view?usp=drive_link Jean-Yves Girard, Proofs and Types] |
# [https://plfa.github.io/ Philip Wadler, Wen Kokke, Jeremy G. Siek, Programming Language Foundations in Agda] | # [https://plfa.github.io/ Philip Wadler, Wen Kokke, Jeremy G. Siek, Programming Language Foundations in Agda] | ||
Текущая версия на 19:15, 18 ноября 2025
Содержание
Типы в языках программирования
Осенний курс по выбору для студентов 3 и 4 курсов ПМИ ФКН ВШЭ.
Лектор: Павел Соколов aka @TurtlePU.
Семинарист: Илья Григорьев aka @ilyagribun.
Ассистент: Ислам Талипов aka @lishy2.
Полезные ссылки
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.
Литература
Основная литература
- Benjamin C. Pierce, Types and Programming Languages
- Frank Pfenning, Lecture Notes on Bidirectional Type Checking
- Jean-Yves Girard, Proofs and Types
- Philip Wadler, Wen Kokke, Jeremy G. Siek, Programming Language Foundations in Agda
