Groupoid Infinity

The Language of Space

TRUSTED SYSTEMS

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.

STRUCTURE

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

TRANSFORMATIONS

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


PUBLICATIONS

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