Groupoid Infinity

The Language of Space


The conceptual model of theorem proving system is presented here as a set of: 1) calculuses with their categorical models; 2) programs or base libraries; and 3) program transformations: type checking, compilation, code erasure, extraction, optimization, etc. The overall system is for math and general purpose programming with code extraction to functional programming languages.


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


The process of formal verification has following phases: model encoding (1), linking with base library of math components (2), desugaring to pure functions (6), linking with pure base library (3), and extracting either to Erlang (4) or Verified Interpreter O (5).


Peer-reviewed articles about implementation details and examples of practical applications:

Consistent Pure Type System with Effects for Erlang/OTP

Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory

Mathematical Components for Cubical Syntax