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

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

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

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

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

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

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

[https://us06web.zoom.us/j/86251590102?pwd=lFywtObgkGYNCHmsCYaZ4c7K1qVwFW.1 Основные пары (Zoom)]

[https://us06web.zoom.us/j/81651253347?pwd=nShEHCMavpLZGGnfCeCI4GvB7kwXve.1 Дополнительные пары (Zoom)]

[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 Записи занятий (Я.Диск)]

[https://classroom.google.com/c/NjM0MDcwNzgzODA3?cjc=rt3n6dq classroom для сдачи заданий]

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

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

* '''Лекция 1, 25 сен 2023'''. Организация курса; Формальные методы и теория типов; Язык IntBool. [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-09-25T08-11-14Z.mp4 Запись].
* '''Семинар 1, 25 сен 2023'''. Денотационная и операционная семантики; Корректность системы типов языка IntBool. [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-09-25T10-01-30Z.mp4 Запись].
* '''Лекция 2, 25 сен 2023'''. Preservation и progress теоремы; Лямбда-исчисление и его Тьюринг-полнота. [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-09-25T11-44-16Z.mp4 Запись].
* '''Семинар 2, 2 окт 2023'''. Операционная семантика лямбда-исчисления; STLC. [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-02T07-55-00Z.mp4 Запись].
* '''Лекция 3, 2 окт 2023'''. Теоретико-множественная семантика STLC; Алгебраические типы данных; Соответствие Карри-Говарда. [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-02T09-56-33Z.mp4 Запись].
* '''Семинар 3, 2 окт 2023'''. Доказательства в интуиционистской логике через CHC; Оператор fix и натуральные числа в STLC. [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-02T11-38-54Z.mp4 Запись].
* '''Лекция 4, 9 окт 2023'''. Оператор явной типизации; типизация параметров в STLC. Полиморфизм и System F; лямбда-куб. [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-09T08-13-25Z.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, 16 окт 2023'''. Система типов Хиндли-Милнера и алгебраические типы данных. Полиморфная рекурсия. [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-16T08-10-51Z.mp4 Запись].
* '''Лекция 6, 16 окт 2023'''. Система типов Хиндли-Милнера и отношение подтипизации. [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-16T10-01-51Z.mp4 Запись].
* '''Семинар 6, 16 окт 2023'''. Тип-пересечение и тип-объединение. Задача эквивалентности типов. Двусторонний вывод типов. [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-16T11-40-03Z.mp4 Запись].

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

* ПДЗ-1 (практическое). Реализация программы, обманывающей систему типов одного из мейнстримных языков программирования. 5 баллов за реализацию, 5 баллов за объяснение. [https://docs.google.com/document/d/1Kkrbkes6KJm_ivMUTqKtqaCd2et55RLBpi3UINhctaA/edit?usp=sharing Условие]. Дедлайн: '''7 ноября в 23:59'''.
* ТДЗ-1 (теоретическое). Решение теоретических задач по темам первой части курса. До 15 баллов. [https://drive.google.com/file/d/12vgTJwM0y5Ollp2kcLgcwLW-qUEgdZyg/view?usp=sharing Условие]. [https://drive.google.com/file/d/1YkJ3aIMn4AqanWAkKym56k0drAMYeZlH/view?usp=sharing Исходник]. Дедлайн: '''23 декабря в 23:59'''.
* ПДЗ-2 (практическое). Реализация алгоритма W с различными расширениями. Базовая реализация 10 баллов, расширения – до 5 бонусных баллов. [https://drive.google.com/file/d/17LTaOWpcXnjI3ICKpfOzyVcy0D6y7byf/view?usp=sharing Условие]. [https://codeforces.com/contestInvitation/ee8782d41e94a66154507098dbbce4ab0c8603e4 Тестирующая система]. Дедлайн: '''30 ноября в 23:59'''.
* ТДЗ-2 (теоретическое). Решение теоретических задач по темам второй части курса. До 15 баллов. [https://drive.google.com/file/d/12vgTJwM0y5Ollp2kcLgcwLW-qUEgdZyg/view?usp=sharing Условие]. [https://drive.google.com/file/d/1YkJ3aIMn4AqanWAkKym56k0drAMYeZlH/view?usp=sharing Исходник]. Дедлайн: '''23 декабря в 23:59'''.
* ПДЗ-3 (практическое, бонусное). Реализация двусторонней проверки типов. 5 бонусных баллов с весом 0.2 в итоге. [https://docs.google.com/document/d/1WGAjqRF2IjsveFyU7hSTKqTWgXO5dVfgqnDO_Ma-Jxo/edit?usp=sharing Условие]. Дедлайн: '''23 декабря в 23:59'''.

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

=== Правила устной сдачи ===

Для сдачи теоретического задания доступна также устная сдача. Для того, чтобы сдать задачу устно, нужно:

# Заранее выписать на лист бумаги или в .pdf все логические правила вывода и термы, необходимые для Вашего решения, а также всё, что должно быть '''выписано''' или '''построено''' по условию задачи;
# Договориться со мной (Павлом) о сдаче во время консультаций (пн-пт с 15 до 18 кроме ср) либо сразу до/после занятия;
# Рассказать решение, опираясь на Ваши выкладки.

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

Итог = Округление(0.1 * ПДЗ-1 + 0.2 * ПДЗ-2 + 0.2 * ПДЗ-3 + 0.25 * ТДЗ-1 + 0.25 * ТДЗ-2).

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

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

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

# 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]

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

# [https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf Lectures on the Curry-Howard Isomorphism]