I'm happy to share Erlang engineering and Type Theory knowledge.

1. HoTT Сourse 2018–2019 — intro, video (3 hr).

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


I write mostly about type theory.

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

2. Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory. ICDSIAI. Springer.

3. Issue I: Internalizing Martin-Löf Type Theory (in-progress). PDF.

4. Issue III: Homotopy Type Theory (in-progress). PDF.

5. Issue VIII: Formal Topos on Category of Sets (in-progress). PDF.

6. Mathematical Components (article series). TeX.


I give talks mostly in the Ukrainian language.

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, video.


Here are my formal pure languages and cubical base libraries:

1. PTS: Pure Type System for Erlang: sources.

2. HTS: Homotopy Type System for Erlang: sources.

3. Groupoid Infinity: The Cubical Base Library sources. (Arend, cubicaltt, Agda, Lean).


Here are my attempts to build runtimes and general purpose programming languages (mostly based on untyped interpreters), in reverse chronological order.

1. O: L1 cache-friendly interpreter with AVX vectorization in Rust: sources. (Prototype).

2. Lazy ML interpreter with process calculus in C: sources. (Toy)

3. Io interpreter in C#: sources. (Experimental, listed at iolanguage.org)

4. Lisp interpreter in C#: sources. (International Land Systems, Inc. Production).

5. PL/1 compiler in C#: sources. (BSc)


Here is a series of my domain specific languages for Erlang.

1. BPE: business proccessing language for Erlang: site, sources (MSc, Production).

2. UPL: card processing language for Erlang: sources (Experimental).


This is how I see data language.

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

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


These are my open-source projects.

1. Longchen Nyingthig — tibetan studies.

2. Cubical base library and Groupoid Infinity language.

3. N2O DEV — language and technology agnostic framework for enterprises.