Types 23 — различия между версиями
Материал из Wiki - Факультет компьютерных наук
TurtlePU (обсуждение | вклад) (→Полезные ссылки) |
TurtlePU (обсуждение | вклад) (→Лекции и семинары) |
||
| Строка 19: | Строка 19: | ||
== Лекции и семинары == | == Лекции и семинары == | ||
| − | * | + | * '''Лекция 1, 25 сен 2023'''. Организация курса; Формальные методы и теория типов; Язык IntBool. |
| + | * '''Семинар 1, 25 сен 2023'''. Денотационная и операционная семантики; Корректность системы типов языка IntBool. | ||
| + | * '''Лекция 2, 25 сен 2023'''. Preservation и progress теоремы; Лямбда-исчисление и его Тьюринг-полнота. | ||
| + | * '''Семинар 2, 2 окт 2023'''. Операционная семантика лямбда-исчисления; STLC. | ||
| + | * '''Лекция 3, 2 окт 2023'''. Теоретико-множественная семантика STLC; Алгебраические типы данных; Соответствие Карри-Говарда. | ||
| + | * '''Семинар 3, 2 окт 2023'''. Доказательства в интуиционистской логике через CHC; Оператор fix и натуральные числа в STLC. | ||
== Домашние задания == | == Домашние задания == | ||
== Итоговая оценка за курс == | == Итоговая оценка за курс == | ||
Версия 20:29, 3 октября 2023
Содержание
Типы в языках программирования
Осенний курс по выбору для студентов 4 курса ПМИ ФКН ВШЭ.
Лектор и семинарист: Павел Соколов aka @TurtlePU.
Полезные ссылки
Лекции и семинары
- Лекция 1, 25 сен 2023. Организация курса; Формальные методы и теория типов; Язык IntBool.
- Семинар 1, 25 сен 2023. Денотационная и операционная семантики; Корректность системы типов языка IntBool.
- Лекция 2, 25 сен 2023. Preservation и progress теоремы; Лямбда-исчисление и его Тьюринг-полнота.
- Семинар 2, 2 окт 2023. Операционная семантика лямбда-исчисления; STLC.
- Лекция 3, 2 окт 2023. Теоретико-множественная семантика STLC; Алгебраические типы данных; Соответствие Карри-Говарда.
- Семинар 3, 2 окт 2023. Доказательства в интуиционистской логике через CHC; Оператор fix и натуральные числа в STLC.
