Groupoid Infinity

The Language of Space


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

While being generic blueprint, part of this conceptual model was implemented in various languages, other research reports applied. This research is founded by Synrc Research Center, Kyiv, Ukraine. All works are done under supervision of Pavlo Maslianko, National Technical University of Ukraine Ā«Igor Sikorsky Kyiv Polytechnic InstituteĀ» Faculty of Applied Mathematics.


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).

Simple Model. This model can serve HoTT research, being MLTT/CCHM prover with limited extraction of pure programs.

Extended Model. This model intended to server needs of linkage with $\pi$-calculus runtimes and optionally stream calculuses and fusion engines. Extraction to Erlang or CPS interpreter.


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