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

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
(→‎Домашние задания)
(→‎Домашние задания)
 
(не показано 10 промежуточных версии этого же участника)
Строка 31: Строка 31:
 
* '''Лекция 2, 9 сен 2024'''. Система типов NatBool+Let. Подстановка. Соглашение об именах. Preservation и progress теоремы. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/09.09%20%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F.mp4 Запись].
 
* '''Лекция 2, 9 сен 2024'''. Система типов NatBool+Let. Подстановка. Соглашение об именах. Preservation и progress теоремы. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/09.09%20%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F.mp4 Запись].
 
* '''Семинар 2, 9 сен 2024'''. Семантика с кучей. Эквивалентность семантик с подстановкой и с кучей. Корректность системы типов NatBool+Let. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/09.09%20%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80.mp4 Запись].
 
* '''Семинар 2, 9 сен 2024'''. Семантика с кучей. Эквивалентность семантик с подстановкой и с кучей. Корректность системы типов NatBool+Let. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/09.09%20%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80.mp4 Запись].
−
* '''Лекция 3, 16 сен 2024'''. Нетипизированное лямбда-исчисление. Стратегии редукции. Теорема Чёрча-Россера. [ Запись].
+
* '''Лекция 3, 16 сен 2024'''. Нетипизированное лямбда-исчисление. Стратегии редукции. Теорема Чёрча-Россера. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202024-09-16T11-56-36Z.mp4 Запись].
−
* '''Семинар 3, 16 сен 2024'''. Кодирование Чёрча для типов данных: логические значения, пары, натуральные числа, списки. Комбинатор неподвижной точки. [ Запись].
+
* '''Семинар 3, 16 сен 2024'''. Кодирование Чёрча для типов данных: логические значения, пары, натуральные числа, списки. Комбинатор неподвижной точки. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202024-09-16T15-02-10Z.mp4 Запись].
−
* '''Лекция 4, 23 сен 2024'''. TBA. [ Запись].
+
* '''Лекция 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'''. TBA. [ Запись].
+
* '''Семинар 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'''. TBA. [ Запись].
+
* '''Лекция 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'''. TBA. [ Запись].
+
* '''Семинар 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'''. TBA. [ Запись].
+
* '''Лекция 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'''. TBA. [ Запись].
+
* '''Семинар 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'''. TBA. [ Запись].
+
* '''Лекция 7, 14 окт 2024'''. Система типов Хиндли-Милнера. Декларативные правила вывода. [ Запись].
−
* '''Семинар 7, 14 окт 2024'''. TBA. [ Запись].
+
* '''Лекция 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 Запись].
−
* '''Лекция 8, 21 окт 2024'''. TBA. [ Запись].
+
* '''Семинар 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 Запись].
−
* '''Семинар 8, 21 окт 2024'''. TBA. [ Запись].
+
* '''Лекция 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. Полиморфная рекурсия. [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 с подтипизацией. [ Запись].
 +
* '''Семинар 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. [https://drive.google.com/file/d/1e5iTyjbkPKIABjm4tQHwdzMoW1OVYoma/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1gkqzoSl_h1E2pDWnNn3kDfkN76AeWf8n/view?usp=drive_link Исходник]. Дедлайн: '''26 сентября 2024 в 23:59'''.
 
* ТДЗ-1 (теоретическое). Система типов IntBool+Let. [https://drive.google.com/file/d/1e5iTyjbkPKIABjm4tQHwdzMoW1OVYoma/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1gkqzoSl_h1E2pDWnNn3kDfkN76AeWf8n/view?usp=drive_link Исходник]. Дедлайн: '''26 сентября 2024 в 23:59'''.
−
* ТДЗ-2 (теоретическое). Тьюринг-полнота нетипизированного лямбда-исчисления. [https://drive.google.com/file/d/13SsC9fjrJwqGT4d5wqcL7zMdwbbaW43_/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1mlBWX8HIrGEsP40NCK1Q9mbqhw9LvLIr/view?usp=drive_link Исходник]. Дедлайн: '''30 сентября 2024 в 23:59'''.
+
* ТДЗ-2 (теоретическое). Тьюринг-полнота нетипизированного лямбда-исчисления. [https://drive.google.com/file/d/13SsC9fjrJwqGT4d5wqcL7zMdwbbaW43_/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1mlBWX8HIrGEsP40NCK1Q9mbqhw9LvLIr/view?usp=drive_link Исходник]. Дедлайн: '''3 октября 2024 в 23:59'''.
−
* ТДЗ-3 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: '''TBA'''.
+
* ТДЗ-3 (теоретическое). Алгебраические типы данных и соответствие Карри-Говарда. [https://drive.google.com/file/d/1lloVL7bqNmihxQOfCBp-7U7u3mzQTXNR/view?usp=sharing Условие]. [https://drive.google.com/file/d/1wLlLtCkHWNQ9OOLB4kkJHTWj2C-8Ktn9/view?usp=sharing Исходник]. Дедлайн: '''18 октября 2024 в 23:59'''.
−
* ПДЗ-1 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.
+
* ПДЗ-1 (практическое). '''СНИМАЕТСЯ'''. Оценка за ПДЗ-1 равна максимальной среди оценок за ПДЗ 2-4.
−
* ПДЗ-2 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.
+
* ПДЗ-2 (практическое). Реализация алгоритма W с различными расширениями. [https://codeforces.com/contestInvitation/220b1b76e428cec54588cf6e75e69c1c3c030f29 Контест]. Дедлайн: '''9 декабря в 23:59'''.
−
* БТДЗ (бонусное теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: '''TBA'''.
+
* БТДЗ (бонусное теоретическое). Строковый полиморфизм. [https://drive.google.com/file/d/1T9N_3AMeNytaa6tIIa447A58fyuuyVMp/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1F6GqFKtXI7zQexGc1nz213D8aIH8if2w/view?usp=drive_link Исходник]. Дедлайн: '''2 декабря в 23:59'''.
 
* ПДЗ-3 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.
 
* ПДЗ-3 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.
 
* ПДЗ-4 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.
 
* ПДЗ-4 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.

Текущая версия на 00:14, 19 ноября 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 (практическое). СНИМАЕТСЯ. Оценка за ПДЗ-1 равна максимальной среди оценок за ПДЗ 2-4.
  • ПДЗ-2 (практическое). Реализация алгоритма W с различными расширениями. Контест. Дедлайн: 9 декабря в 23:59.
  • БТДЗ (бонусное теоретическое). Строковый полиморфизм. Условие. Исходник. Дедлайн: 2 декабря в 23:59.
  • ПДЗ-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=88107»