В рамках курса по функциональному программированию для ИУ9-11М в Москву приедет @fizruk (Николай Кудасов), чтобы 20 и 21 ноября провести интенсив по HoTT (ака Homotopy Type Theory).
Интенсив будет проходить два дня с 10 до 19, и включать в себя практическую часть: построение доказательств посредством Proof Assistant. Целью интенсива является прежде всего знакомство с современной концепцией типа (в алгебраическом и теоретико-категорном ключе), формализацией математики, и освоение понятия зависимых типов.
- Магистрантам участие в интенсиве (в практической части) засчитывается за лабораторную работу (как зачётную единицу) и 5 баллов за модуль, но при достаточной активности в решении задач можно нафармить до 15 баллов.
- 3 курс (ТФЯ) активное участие в практической части - 5 баллов авансом за компромат на экзамене. Или 5 баллов сверх семестровых при зачёте на автомат (то есть на автомат будет достаточно набрать 85 баллов вместо 90 за семестр).
- Базовые представления о лямбда-исчислении и алгебраических типах данных (стрелочный тип, кортежный тип, карринг)
- Базовое знание логики первого порядка
- Знание абстрактной алгебры (на уровне одного семестра ИУ9 вполне достаточно)
- Умение написать на Haskell простую функциональную программу
Желающие участвовать в воркшопе (прежде всего, с бакалавриата ИУ9) могут запросить дополнительный подготовительный семинар (или два), по согласованию.
- Читаем первую главу HoTT: https://hott.github.io/book/hott-online-7-g6913a1a.pdf (до Identity types)
- Устанавливаем rzk, можно через VScode extensions