Онлайн-курс «Современные теории типов»

В среду 15 июля в 19:00 CEST/UTC+2 (20:00 MSK) в Лаборатории формальной математики стартует курс по современным теориям типов. Лекции читают @akuklev и @clayrat по средам, примерно по часу, частота - раз в неделю (с летними пропусками). Начнём с обзора формальных языков и алгебраических теорий и пойдём до самого фронтира синтетических и направленных теорий типов. Примерная программа:

1. Вводная лекция
2. Языки и алгебраические теории
3. STLC и System T
4. PCF
5. System F и Fω
6. Зависимо-типизированные языки
7. Индукция
8. Рефайнмент- и фактор-типы
9. Эффекты в типах
10. HoTT
11. OTT/CuTT
12. □-полиморфизм
13. Модальные типы
14. Охраняемая рекурсия
15. Когезивные модальности
16. Направленные и симплициальные теории

Не требуется предварительной подготовки по теории типов, но пригодятся базовые познания в функциональном программировании и алгебре. Знание теории категорий для понимания курса в целом не нужно, за одним исключением: мы будем обсуждать внутренние языки категорий и топосов (определение топоса дадим по ходу), где не помешает помнить определение декартово замкнутой категории.

Ссылка на гугл-календарь, где будем публиковать даты лекций:
https://calendar.google.com/calendar/u/0?cid=YzdkMGI0MTdlZjFiMTg1OGVmNzUyYjFkZjBjYjYwZjBhYTI0MGExNjlhMWVhZGY5OTcyOGYwOTM4OTVlMDliM0Bncm91cC5jYWxlbmRhci5nb29nbGUuY29t

Тот же календарь, в формате .ics
https://calendar.google.com/calendar/ical/c7d0b417ef1b1858ef752b1df0cb60f0aa240a169a1eadf99728f093895e09b3%40group.calendar.google.com/public/basic.ics