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

Александр Грызлов, IMDEA Software Institute, Spain
Александр Куклев, Radboud University Nijmegen, Software Science, JetBrains Research

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

  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. Направленные и симплициальные теории

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