Maxim Sokhatsky

National Technical University of Ukraine
«Igor Sikorsky Kyiv Polytechnic Institute»
Faculty of Applied Mathematics
Adress: Building 14 (Applied Mathematics),
Polytechnichna str. 14-A, Kyiv, Ukraine, 03056.
Telephone: +380442048115.

I am a Ph.D. student in the Applied Mathematics Faculty at National Technical University of Ukraine «Igor Sikorsky Kyiv Polytechnic Institute». I received MSc at same place with «Business Process Engine: Theory and Implementation» work, which was later adopted to production as BPE in PrivatBank, one of the biggest bank in Eastern Europe. Before I received BSc at same place with «PL/1: Design and Implementation for .NET CLR». All my academic works are done under supervision of Pavlo Maslianko.

My current research interests focus on cubical type checkers and formalization of mathematics. I do love code in cubicaltt, but respect other HoTT provers, like yacctt, RedPRL, agda --cubical. Also I love to create programming languages.


1. HoTT Сourse 2018–2019 — intro

2. Erlang Courses 2013–2014 — video (12 hrs).


1. The Systems Engineering of Consistent Pure Language with Effect Type System for Certified Applications and Higher Languages. MMCTSE. TeX, PDF

2. Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory. ICDSIAI. TeX, PDF

3. Mathematical Components for Cubical Syntax (in-progress). TeX, PDF

Talks (Ukrainian)

1. MLTT Intro and Categorical Semantics of Inductive Types: video

2. Presentation of cubicaltt by Anders Mörtberg et all: video 1, video 2.

3. Cubical Live Coding (MLTT Rules): video

4. f(cafe): The Language of Space: slides

Pure Languages

1. Groupoid Infinity: The Language of Space: sources. (Mathematical Components).

2. OM: Consistent PTS with Universes for Erlang: sources. (Academic, Educational, Teaching).

General Purpose Languages

1. O: L1 sized byte code interpreter with AVX Vectorization in Rust: sources. (Prototype).

2. Joxa modification for Erlang AST compilation: sources. (Toy)

3. Lazy ML with Process Calculus in C: sources. (Toy)

4. Io for .NET: sources. (Experimental, listed at

5. Lisp for .NET: sources. (International Land Systems, Inc. Production).

6. PL/1 .NET: sources. (BSc)

Domain Specific Languages

1. BPE for Erlang: site, sources (Production).

2. N2O for Erlang: site, sources (Production).
    One of the top open source Erlang project, used in numerous startups around the world.

3. UPL for Erlang: sources (Experimental).


1. Chain Replication Database for Erlang: article, sources. (Experimental).

2. KVS Database Abstraction Layer for Erlang: site, sources (Production).

Web Sites (by Arseniy Bushyn)

1. Longchen Nyingthig: site

2. Groupoid Infinity: site

3. N2O Ecosystem: site

4. Operating System with immutable CAS queues and K flavored Programming Language: site

Namdak Tonpa © 2016—2018.