Types 23 — различия между версиями
Материал из Wiki - Факультет компьютерных наук
TurtlePU (обсуждение | вклад) (→Итоговая оценка за курс) |
TurtlePU (обсуждение | вклад) (→Лекции и семинары) |
||
| Строка 28: | Строка 28: | ||
* '''Семинар 4, 9 окт 2023'''. Система типов Хиндли-Милнера, часть 1. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%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%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-10-09T09-59-36Z.mp4 Запись]. | * '''Семинар 4, 9 окт 2023'''. Система типов Хиндли-Милнера, часть 1. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%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%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-10-09T09-59-36Z.mp4 Запись]. | ||
* '''Лекция 5, 9 окт 2023'''. Система типов Хиндли-Милнера, часть 2. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%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%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-10-09T11-36-41Z.mp4 Запись]. | * '''Лекция 5, 9 окт 2023'''. Система типов Хиндли-Милнера, часть 2. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%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%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-10-09T11-36-41Z.mp4 Запись]. | ||
| + | * '''Семинар 5, 16 окт 2023'''. Система типов Хиндли-Милнера и алгебраические типы данных. Полиморфная рекурсия. [Запись]. | ||
| + | * '''Лекция 6, 16 окт 2023'''. Система типов Хиндли-Милнера и отношение подтипизации. [Запись]. | ||
| + | * '''Семинар 6, 16 окт 2023'''. Тип-пересечение и тип-объединение. Задача эквивалентности типов. Двусторонний вывод типов. [Запись]. | ||
== Домашние задания == | == Домашние задания == | ||
Версия 18:04, 16 октября 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. Запись.
- Лекция 4, 9 окт 2023. Оператор явной типизации; типизация параметров в STLC. Полиморфизм и System F; лямбда-куб. Запись.
- Семинар 4, 9 окт 2023. Система типов Хиндли-Милнера, часть 1. Запись.
- Лекция 5, 9 окт 2023. Система типов Хиндли-Милнера, часть 2. Запись.
- Семинар 5, 16 окт 2023. Система типов Хиндли-Милнера и алгебраические типы данных. Полиморфная рекурсия. [Запись].
- Лекция 6, 16 окт 2023. Система типов Хиндли-Милнера и отношение подтипизации. [Запись].
- Семинар 6, 16 окт 2023. Тип-пересечение и тип-объединение. Задача эквивалентности типов. Двусторонний вывод типов. [Запись].
Домашние задания
- ПДЗ-1 (практическое). TBA
- ТДЗ-1 (теоретическое). TBA
- ПДЗ-2 (практическое). TBA
- ТДЗ-2 (теоретическое). TBA
- ПДЗ-3 (практическое). TBA
Итоговая оценка за курс
Итог = Округление(0.1 * ПДЗ-1 + 0.2 * ПДЗ-2 + 0.2 * ПДЗ-3 + 0.25 * ТДЗ-1 + 0.25 * ТДЗ-2).
Округление арифметическое.
