Гомотопическая теория типов

Закрытая рабочая группа собирается, чтобы обсуждать и ботать HoTT, Coq и другие штуки. Здесь нет ведущего, нет лектора. Это именно колернинг, рабочая группа, где каждый сам делает так, чтобы встречи имели для него смысл и пользу.

На прошлых встречах обсуждали, например, такие вещи:

• индуктивные принципы
• соответствие Карри-Говарда
• принцип Propositions as Types
• в чём сходство, а в чём различие между высказываниями и типами
• как работают и на каких принципах основаны системы доказательства теорем (Coq)
• что вообще можно делать в Coq
• как в нём поудобнее делать то, что мы хотим (например: формализовать понятия общей алгебры; формализовать анализ функций; доказать Гёделя о неполноте, замостить плоскость Лобачевского семиугольниками)
• что такое гомотопическая теория типов, как можно геометрически думать о равенствах и доказательствах
• темпоральную логику

Из вещей, о которых участники знают меньше, но любопытствуют: кубическая теория типов, теория категорий, Isabelle/HOL.

Как присоединиться к группе?

Сейчас группа в Кочерге не собирается.

Вопросы по группе можно задать в телеграм @mrgutkun.