Groupoid Infinity

The Language of Space


Here is presented the conceptual model of theorem proving system as a set of 1) calculuses with its categorical models; 2) programs or base libraries; and 3) program transformations: type checking, compilation, code erasure, extraction, optimizing, etc. The overal system is dedicated for math and general purpose programming with code extraction to functional programming language compilers or interpreters.


The thesis is grouped by research areas with its corresponding type systems, formal models, type checkers and base libraries.


The process of formal verification is started from model encoding (1), then linking with the base library of math components (2), then desugaring to pure functions (6), then linking with pure base library (3), then extracting either to Erlang (4) or Verified Interpreter O (5).


Peer-reviewed articles about implementation details and practical usage:

Consistent Pure Type System with Effects for Erlang/OTP

Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory

Mathematical Components for Cubical Syntax