Кочерга

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

Закрытая группа для освоения прикладной верификации, гомотопической теории типов и других штук.

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

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

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

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

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

Спросите себя, готовы ли вы регулярно ходить и самостоятельно учиться, и если готовы, напишите об этом на oknezrob@kocherga-club.ru или в телеграм @mrgutkun.