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

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
(→‎Лекции и семинары)
(→‎Лекции и семинары)
Строка 35: Строка 35:
 
* '''Лекция 4, 23 сен 2024'''. Просто типизированное лямбда-исчисление. Доказательство слабой нормализуемости. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202024-09-23T11-36-06Z%20(1).mp4 Запись].
 
* '''Лекция 4, 23 сен 2024'''. Просто типизированное лямбда-исчисление. Доказательство слабой нормализуемости. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202024-09-23T11-36-06Z%20(1).mp4 Запись].
 
* '''Семинар 4, 23 сен 2024'''. Теоретико-множественная семантика STLC. Логическая семантика STLC. Пустой тип. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202024-09-23T14-55-33Z%20(1).mp4 Запись].
 
* '''Семинар 4, 23 сен 2024'''. Теоретико-множественная семантика STLC. Логическая семантика STLC. Пустой тип. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202024-09-23T14-55-33Z%20(1).mp4 Запись].
−
* '''Лекция 5, 30 сен 2024'''. Вычисления с сайд-эффектами: исключения, состояние, I/O. [ Запись].
+
* '''Лекция 5, 30 сен 2024'''. Вычисления с сайд-эффектами: исключения, состояние, I/O. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202024-09-30T11-41-27Z%20(3).mp4 Запись].
−
* '''Семинар 5, 30 сен 2024'''. Изо- и экви- рекурсивные типы данных. Корректность для систем с сайд-эффектами и рекурсией. [ Запись].
+
* '''Семинар 5, 30 сен 2024'''. Изо- и экви- рекурсивные типы данных. Корректность для систем с сайд-эффектами и рекурсией. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202024-09-30T14-59-58Z%20(3).mp4 Запись].
−
* '''Лекция 6, 7 окт 2024'''. Полиморфизм и System F. Лямбда-куб. [ Запись].
+
* '''Лекция 6, 7 окт 2024'''. Полиморфизм и System F. Лямбда-куб. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202024-10-07T11-38-07Z%20(1).mp4 Запись].
−
* '''Семинар 6, 7 окт 2024'''. Выразительность System F: алгебраические типы данных, Nat. [ Запись].
+
* '''Семинар 6, 7 окт 2024'''. Выразительность System F: алгебраические типы данных, Nat. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202024-10-07T15-04-47Z%20(1).mp4 Запись].
 
* '''Лекция 7, 14 окт 2024'''. Система типов Хиндли-Милнера. Декларативные правила вывода. [ Запись].
 
* '''Лекция 7, 14 окт 2024'''. Система типов Хиндли-Милнера. Декларативные правила вывода. [ Запись].
−
* '''Лекция 8, 21 окт 2024'''. Операторы на типах. Система кайндов. [ Запись].
+
* '''Лекция 8, 21 окт 2024'''. Операторы на типах. Система кайндов. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202024-10-21T11-42-07Z.mp4 Запись].
−
* '''Семинар 7, 21 окт 2024'''. Унификация. Алгоритмы J и W. Расширения системы Хиндли-Милнера. [ Запись].
+
* '''Семинар 7, 21 окт 2024'''. Унификация. Алгоритмы J и W. Расширения системы Хиндли-Милнера. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202024-10-21T15-08-27Z.mp4 Запись].
−
* '''Лекция 9, 11 ноя 2024'''. Отношение подтипизации. Решётка типов для STLC. [ Запись].
+
* '''Лекция 9, 11 ноя 2024'''. Отношение подтипизации. Решётка типов для STLC. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202024-11-11T11-46-25Z.mp4 Запись].
−
* '''Семинар 8, 11 ноя 2024'''. Операторы на типах в системе HM. Полиморфная рекурсия. [ Запись].
+
* '''Семинар 8, 11 ноя 2024'''. Операторы на типах в системе HM. Полиморфная рекурсия. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202024-11-11T15-00-57Z.mp4 Запись].
 
* '''Лекция 10, 18 ноя 2024'''. Двусторонний вывод типов для STLC с подтипизацией.
 
* '''Лекция 10, 18 ноя 2024'''. Двусторонний вывод типов для STLC с подтипизацией.
 
* '''Семинар 9, 18 ноя 2024'''. Ковариантность и контравариантность. Вывод типов для систем с подтипизацией. [ Запись].
 
* '''Семинар 9, 18 ноя 2024'''. Ковариантность и контравариантность. Вывод типов для систем с подтипизацией. [ Запись].

Версия 22:21, 18 ноября 2024

Типы в языках программирования

Осенний курс по выбору для студентов 3 и 4 курсов ПМИ ФКН ВШЭ.

Лектор: Павел Соколов aka @TurtlePU.

Семинарист: Илья Григорьев aka @ilyagribun.

Ассистент: Яна Ике aka @jijasan.

Полезные ссылки

Канал курса (Telegram)

Чат курса (Telegram)

Лекции (Zoom)

Семинары (Zoom)

Записи занятий (Я.Диск)

classroom для сдачи теоретических домашних заданий

Оценки

Лекции и семинары

  • Лекция 1, 2 сен 2024. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. Запись.
  • Семинар 1, 2 сен 2024. Операционные семантики; Эквивалентности семантик; Preservation и Progress теоремы; Корректность системы типов относительно операционной семантики. Запись.
  • Лекция 2, 9 сен 2024. Система типов NatBool+Let. Подстановка. Соглашение об именах. Preservation и progress теоремы. Запись.
  • Семинар 2, 9 сен 2024. Семантика с кучей. Эквивалентность семантик с подстановкой и с кучей. Корректность системы типов NatBool+Let. Запись.
  • Лекция 3, 16 сен 2024. Нетипизированное лямбда-исчисление. Стратегии редукции. Теорема Чёрча-Россера. Запись.
  • Семинар 3, 16 сен 2024. Кодирование Чёрча для типов данных: логические значения, пары, натуральные числа, списки. Комбинатор неподвижной точки. Запись.
  • Лекция 4, 23 сен 2024. Просто типизированное лямбда-исчисление. Доказательство слабой нормализуемости. Запись.
  • Семинар 4, 23 сен 2024. Теоретико-множественная семантика STLC. Логическая семантика STLC. Пустой тип. Запись.
  • Лекция 5, 30 сен 2024. Вычисления с сайд-эффектами: исключения, состояние, I/O. Запись.
  • Семинар 5, 30 сен 2024. Изо- и экви- рекурсивные типы данных. Корректность для систем с сайд-эффектами и рекурсией. Запись.
  • Лекция 6, 7 окт 2024. Полиморфизм и System F. Лямбда-куб. Запись.
  • Семинар 6, 7 окт 2024. Выразительность System F: алгебраические типы данных, Nat. Запись.
  • Лекция 7, 14 окт 2024. Система типов Хиндли-Милнера. Декларативные правила вывода. [ Запись].
  • Лекция 8, 21 окт 2024. Операторы на типах. Система кайндов. Запись.
  • Семинар 7, 21 окт 2024. Унификация. Алгоритмы J и W. Расширения системы Хиндли-Милнера. Запись.
  • Лекция 9, 11 ноя 2024. Отношение подтипизации. Решётка типов для STLC. Запись.
  • Семинар 8, 11 ноя 2024. Операторы на типах в системе HM. Полиморфная рекурсия. Запись.
  • Лекция 10, 18 ноя 2024. Двусторонний вывод типов для STLC с подтипизацией.
  • Семинар 9, 18 ноя 2024. Ковариантность и контравариантность. Вывод типов для систем с подтипизацией. [ Запись].
  • Лекция 11, 25 ноя 2024. TBA. [ Запись].
  • Семинар 11, 25 ноя 2024. TBA. [ Запись].
  • Лекция 12, 2 дек 2024. TBA. [ Запись].
  • Семинар 12, 2 дек 2024. TBA. [ Запись].
  • Лекция 13, 9 дек 2024. TBA. [ Запись].
  • Семинар 13, 9 дек 2024. TBA. [ Запись].
  • Лекция 14, 16 дек 2024. TBA. [ Запись].
  • Семинар 14, 16 дек 2024. TBA. [ Запись].

Домашние задания

  • ТДЗ-1 (теоретическое). Система типов IntBool+Let. Условие. Исходник. Дедлайн: 26 сентября 2024 в 23:59.
  • ТДЗ-2 (теоретическое). Тьюринг-полнота нетипизированного лямбда-исчисления. Условие. Исходник. Дедлайн: 3 октября 2024 в 23:59.
  • ТДЗ-3 (теоретическое). Алгебраические типы данных и соответствие Карри-Говарда. Условие. Исходник. Дедлайн: 18 октября 2024 в 23:59.
  • ПДЗ-1 (практическое). TBA. [ Условие]. Дедлайн: TBA.
  • ПДЗ-2 (практическое). TBA. [ Условие]. Дедлайн: TBA.
  • БТДЗ (бонусное теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: TBA.
  • ПДЗ-3 (практическое). TBA. [ Условие]. Дедлайн: TBA.
  • ПДЗ-4 (практическое). TBA. [ Условие]. Дедлайн: TBA.
  • БПДЗ (бонусное практическое). TBA. [ Условие]. Дедлайн: TBA.
  • ТДЗ-4 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: TBA.

Условие теоретических домашних заданий скомпилировано с помощью pdfLaTeX.

Итоговая оценка за курс

Итог = Округление(0.4 * ТДЗ + 0.6 * ПДЗ + Б),

где ТДЗ – средняя оценка за теоретические домашние задания, ПДЗ – за практические, а Б – сумма бонусных баллов, полученных за курс.

Округление арифметическое.

Литература

Основная литература

  1. Benjamin C. Pierce, Types and Programming Languages
  2. Frank Pfenning, Lecture Notes on Bidirectional Type Checking
  3. Jean-Yves Girard, Proofs and Types

Дополнительная литература

  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_24&oldid=88094»