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 (4).
Minimal Model. This model can serve HoTT research, being MLTT/CCHM prover with limited extraction of pure programs to certified interpreter.
Cubical Model. This model can serve HoTT research, being MLTT/CCHM prover with limited extraction of pure programs to certified interpreter.
Spectral 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.
Fascicule de Résultats
Peer-reviewed articles about homotopy type theory foundations and formalization of mathematics, implementation details and examples of practical applications: