Types 25 — различия между версиями
Материал из Wiki - Факультет компьютерных наук
TurtlePU (обсуждение | вклад) (→Полезные ссылки) |
TurtlePU (обсуждение | вклад) (→Лекции и семинары) |
||
| Строка 33: | Строка 33: | ||
* '''Лекция 1, 16 сен 2025'''. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [TBA Запись]. | * '''Лекция 1, 16 сен 2025'''. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [TBA Запись]. | ||
* '''Семинар 1, 19 сен 2025'''. Small-step и big-step операционная семантика языка NatBool; Эквивалентность семантик; Свойства Preservation и Progress; Здравость системы типов относительно операционной семантики. [TBA Запись]. | * '''Семинар 1, 19 сен 2025'''. Small-step и big-step операционная семантика языка NatBool; Эквивалентность семантик; Свойства Preservation и Progress; Здравость системы типов относительно операционной семантики. [TBA Запись]. | ||
| − | * '''Лекция 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 и её эквивалентность семантике с подстановкой; Присваивания и циклы. [TBA Запись]. | * '''Семинар 2, 23 сен 2025'''. Семантика с бэгами для NatBool+Let и её эквивалентность семантике с подстановкой; Присваивания и циклы. [TBA Запись]. | ||
| − | * '''Лекция 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'''. Погружение одной системы в другую; Кодирование Чёрча; Нумералы Чёрча; Логические значения, кортежи и списки в лямбда-исчислении; Комбинатор неподвижной точки и его вывод. [TBA Запись]. | * '''Семинар 3, 30 сен 2025'''. Погружение одной системы в другую; Кодирование Чёрча; Нумералы Чёрча; Логические значения, кортежи и списки в лямбда-исчислении; Комбинатор неподвижной точки и его вывод. [TBA Запись]. | ||
* '''Лекция 4, 7 окт 2025''' (online). TBA. [TBA Конспект] [TBA Запись]. | * '''Лекция 4, 7 окт 2025''' (online). TBA. [TBA Конспект] [TBA Запись]. | ||
Версия 14:07, 2 октября 2025
Содержание
Типы в языках программирования
Осенний курс по выбору для студентов 3 и 4 курсов ПМИ ФКН ВШЭ.
Лектор: Павел Соколов aka @TurtlePU.
Семинарист: Илья Григорьев aka @ilyagribun.
Ассистент: Ислам Талипов aka @lishy2.
Полезные ссылки
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 относительно операционной семантики. Запись.
- Семинар 2, 23 сен 2025. Семантика с бэгами для NatBool+Let и её эквивалентность семантике с подстановкой; Присваивания и циклы. [TBA Запись].
- Лекция 3, 30 сен 2025. Бета-редукция и подстановка в лямбда-исчислении; Нормальные формы; Альфа- и эта- эквивалентность; Конфлюэнтность лямбда-исчисления. Конспект Запись.
- Семинар 3, 30 сен 2025. Погружение одной системы в другую; Кодирование Чёрча; Нумералы Чёрча; Логические значения, кортежи и списки в лямбда-исчислении; Комбинатор неподвижной точки и его вывод. [TBA Запись].
- Лекция 4, 7 окт 2025 (online). TBA. [TBA Конспект] [TBA Запись].
- Семинар 4, 7 окт 2025. TBA. [TBA Запись].
Домашние задания
- ТДЗ-1 (теоретическое). Система IntBool+Let. Условие. Исходник. Дедлайн: 7 октября в 18:10.
- ТДЗ-2 (теоретическое). Тьюринг-полнота лямбда-исчисления. Условие. Исходник. Дедлайн: 16 октября в 18:10.
- ДЗ-3. 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
