![](data:image/svg+xml;charset=utf-8,<svg width="640" height="640" style="background-color:%2344badc;font-family:Nunito,sans-serif" viewBox="0 0 100 100" preserveAspectRatio="xMidYMid meet" xmlns="http://www.w3.org/2000/svg">
<text font-size="30" x="50%" y="50%" dy="5" fill="white" dominant-baseline="middle" text-anchor="middle">fl</text>
</svg>)
Онлайн-курс «Современные теории типов»
В среду 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
В среду 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