# CONCEPTUAL MODEL

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.

# LANGUAGE FAMILY

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

## Effect System

## $\pi$-Calculus

## MLTT/CCHM

## Stream Calculus

# TRANSFORMATIONS

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.

# PUBLICATIONS

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