Теория типов

InBox

  • Гомотопическая теория типов
  • Интенсиональная теория типов, классическая теория типов Мартин-Лёва (MLTT). Языки Agda и Idris.
  • Исчисление индуктивных конструкций (CIQ). Язык Coq.