Сегодня в 12:00 UTC (через ~1.5 часа) планирую постримить разбор PoC компилятора в пучки.
GitHub
GitHub - aspiwack/sheaf-lang-demo: An experiment to see what interpretation into (pre)sheaves categories look like
An experiment to see what interpretation into (pre)sheaves categories look like - aspiwack/sheaf-lang-demo
👍7🔥5
Формализация краткого вывода закона исключенного третьего из аксиомы выбора (узнал от Валерия Исаева):
https://gist.github.com/clayrat/80f2e048831e6829a49d5cb3843b2c7d
https://gist.github.com/clayrat/80f2e048831e6829a49d5cb3843b2c7d
Gist
AC implies LEM
AC implies LEM. GitHub Gist: instantly share code, notes, and snippets.
🔥6🤯2👍1🙏1
Сегодня в 12:45 UTC (через ~2.5 часа) планирую постримить на ютюб-канале формализацию Symmetry Book на кубических типах.
GitHub
GitHub - UniMath/SymmetryBook: This book will be a textbook written in the univalent style, taking advantage of the presence of…
This book will be a textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage. - UniMath/SymmetryBook
🙏4❤1
Сегодня в 12:30 UTC (через ~2 часа) планирую постримить формализацию понятия рефлексивных графов.
❤1
Forwarded from Alex Gryzlov
Онлайн-курс «Современные теории типов»
В среду 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
В среду 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
Google Workspace
Google Calendar - Easier Time Management, Appointments & Scheduling
Learn how Google Calendar helps you stay on top of your plans - at home, at work and everywhere in between.
❤47
Alex Gryzlov
Онлайн-курс «Современные теории типов» В среду 15 июля в 19:00 CEST/UTC+2 (20:00 MSK) в Лаборатории формальной математики стартует курс по современным теориям типов. Лекции читают @akuklev и @clayrat по средам, примерно по часу, частота - раз в неделю (с…
Первая лекция через час, зум-ссылка в календаре.
👍9🕊2👀2❤1
Forwarded from formal labs
Следующая лекция по теориям типов (STLC и System T) пройдет в среду 5 августа, в то же время (19:00 CEST/UTC+2 / 20:00 MSK).
👍13