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

Онлайн-курс «Современные теории типов» В среду 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