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 about type theory.

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

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

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


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 base libraries with П-types.

1. Groupoid Infinity: The Language of Space: sources. (Cubical Base Library).

2. OM: Morte compiler in Erlang: sources. (Academic).


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. N2O: application protocol language for Erlang: site, sources (Production) — One of the top open-source Erlang projects, used in numerous startups around the world.

3. 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: site.

2. Groupoid Infinity: site.

3. N2O Ecosystem: site.