Просмотр кода страницы Types 24

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

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

'''Лектор''': Павел Соколов aka [https://t.me/TurtlePU @TurtlePU].

'''Семинарист''': Илья Григорьев aka [https://t.me/ilyagribun @ilyagribun].

'''Ассистент''': Яна Ике aka [https://t.me/jijasan @jijasan].

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

[https://t.me/+u5nrljUi_JdiNmRi Канал курса (Telegram)]

[https://t.me/+A7z6pUNQ2AplNWMy Чат курса (Telegram)]

[https://us06web.zoom.us/j/88993803532?pwd=F1aFxf9DY1R81caDQBgGnwcaSstqIj.1 Лекции (Zoom)]

[https://us06web.zoom.us/j/88580149532?pwd=XAtNlbGimHZboYL5bOSSjxO8AUOHmB.1 Семинары (Zoom)]

[https://disk.yandex.ru/d/WhHJyFeb9mDdkA Записи занятий (Я.Диск)]

[https://classroom.google.com/c/NzExNzI1MDg2MjA3?cjc=sihngzs classroom для сдачи теоретических домашних заданий]

[https://docs.google.com/spreadsheets/d/1PIpVuanxZmANMT0Z6wK46Osy5CVVxUIc_-IJhcThf_I/edit?usp=sharing Оценки]

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

* '''Лекция 1, 2 сен 2024'''. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/02.09%20%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F.mp4 Запись].
* '''Семинар 1, 2 сен 2024'''. Операционные семантики; Эквивалентности семантик; Preservation и Progress теоремы; Корректность системы типов относительно операционной семантики. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/02.09%20%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80.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 Запись].
* '''Лекция 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'''. Кодирование Чёрча для типов данных: логические значения, пары, натуральные числа, списки. Комбинатор неподвижной точки. [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'''. Просто типизированное лямбда-исчисление. Доказательство слабой нормализуемости. [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 Запись].
* '''Лекция 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'''. Изо- и экви- рекурсивные типы данных. Корректность для систем с сайд-эффектами и рекурсией. [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. Лямбда-куб. [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. [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'''. Система типов Хиндли-Милнера. Декларативные правила вывода. [ Запись].
* '''Лекция 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. Расширения системы Хиндли-Милнера. [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. [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'''.
* ТДЗ-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 (теоретическое). Алгебраические типы данных и соответствие Карри-Говарда. [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 (практическое). '''СНИМАЕТСЯ'''. Оценка за ПДЗ-1 равна максимальной среди оценок за ПДЗ 2-4.
* ПДЗ-2 (практическое). Реализация алгоритма W с различными расширениями. [https://codeforces.com/contestInvitation/220b1b76e428cec54588cf6e75e69c1c3c030f29 Контест]. Дедлайн: '''9 декабря в 23:59'''.
* БТДЗ (бонусное теоретическое). Строковый полиморфизм. [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'''.
* ПДЗ-4 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.
* БПДЗ (бонусное практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.
* ТДЗ-4 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: '''TBA'''.

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

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

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

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

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

== Литература ==

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

# Benjamin C. Pierce, Types and Programming Languages
# [https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bidirectional.pdf Frank Pfenning, Lecture Notes on Bidirectional Type Checking]
# Jean-Yves Girard, Proofs and Types

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

# [https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf Lectures on the Curry-Howard Isomorphism]
# [http://twelf.org/wiki/Main_Page The Twelf Project]
# [https://lean-lang.org/ Programming Language and Theorem Prover – Lean]
# [https://granule-project.github.io/ The Granule Project]