Types 23 — различия между версиями
Материал из Wiki - Факультет компьютерных наук
TurtlePU (обсуждение | вклад) (→Домашние задания) |
TurtlePU (обсуждение | вклад) (→Домашние задания) |
||
| Строка 40: | Строка 40: | ||
* ПДЗ-1 (практическое). Реализация программы, обманывающей систему типов одного из мейнстримных языков программирования. 5 баллов за реализацию, 5 баллов за объяснение. [https://docs.google.com/document/d/1Kkrbkes6KJm_ivMUTqKtqaCd2et55RLBpi3UINhctaA/edit?usp=sharing Условие]. Дедлайн: '''7 ноября в 23:59'''. | * ПДЗ-1 (практическое). Реализация программы, обманывающей систему типов одного из мейнстримных языков программирования. 5 баллов за реализацию, 5 баллов за объяснение. [https://docs.google.com/document/d/1Kkrbkes6KJm_ivMUTqKtqaCd2et55RLBpi3UINhctaA/edit?usp=sharing Условие]. Дедлайн: '''7 ноября в 23:59'''. | ||
* ТДЗ-1 (теоретическое). Решение теоретических задач по темам первой части курса. До 15 баллов. [Условие]. Дедлайн: TBA. | * ТДЗ-1 (теоретическое). Решение теоретических задач по темам первой части курса. До 15 баллов. [Условие]. Дедлайн: TBA. | ||
| − | * ПДЗ-2 (практическое). Реализация алгоритма W с различными расширениями. Базовая реализация 10 баллов, расширения – до 5 бонусных баллов. [https://drive.google.com/file/d/17LTaOWpcXnjI3ICKpfOzyVcy0D6y7byf/view?usp=sharing Условие]. [https://codeforces.com/contestInvitation/ee8782d41e94a66154507098dbbce4ab0c8603e4 Тестирующая система]. Дедлайн: ''' | + | * ПДЗ-2 (практическое). Реализация алгоритма W с различными расширениями. Базовая реализация 10 баллов, расширения – до 5 бонусных баллов. [https://drive.google.com/file/d/17LTaOWpcXnjI3ICKpfOzyVcy0D6y7byf/view?usp=sharing Условие]. [https://codeforces.com/contestInvitation/ee8782d41e94a66154507098dbbce4ab0c8603e4 Тестирующая система]. Дедлайн: '''30 ноября в 23:59'''. |
* ТДЗ-2 (теоретическое). Решение теоретических задач по темам второй части курса. До 15 баллов. [Условие]. Дедлайн: TBA | * ТДЗ-2 (теоретическое). Решение теоретических задач по темам второй части курса. До 15 баллов. [Условие]. Дедлайн: TBA | ||
* ПДЗ-3 (практическое). Реализация двусторонней проверки типов с различными расширениями. Три вариации до 5 баллов за каждую. [Условие]. Дедлайн: TBA | * ПДЗ-3 (практическое). Реализация двусторонней проверки типов с различными расширениями. Три вариации до 5 баллов за каждую. [Условие]. Дедлайн: TBA | ||
Версия 11:29, 18 ноября 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 (практическое). Реализация программы, обманывающей систему типов одного из мейнстримных языков программирования. 5 баллов за реализацию, 5 баллов за объяснение. Условие. Дедлайн: 7 ноября в 23:59.
- ТДЗ-1 (теоретическое). Решение теоретических задач по темам первой части курса. До 15 баллов. [Условие]. Дедлайн: TBA.
- ПДЗ-2 (практическое). Реализация алгоритма W с различными расширениями. Базовая реализация 10 баллов, расширения – до 5 бонусных баллов. Условие. Тестирующая система. Дедлайн: 30 ноября в 23:59.
- ТДЗ-2 (теоретическое). Решение теоретических задач по темам второй части курса. До 15 баллов. [Условие]. Дедлайн: TBA
- ПДЗ-3 (практическое). Реализация двусторонней проверки типов с различными расширениями. Три вариации до 5 баллов за каждую. [Условие]. Дедлайн: TBA
Итоговая оценка за курс
Итог = Округление(0.1 * ПДЗ-1 + 0.2 * ПДЗ-2 + 0.2 * ПДЗ-3 + 0.25 * ТДЗ-1 + 0.25 * ТДЗ-2).
Округление арифметическое.
Литература
Основная литература
- Benjamin C. Pierce, Types and Programming Languages
- Frank Pfenning, Lecture Notes on Bidirectional Type Checking
