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.

7. Modal Homotopy Type System. Site, PDF, Sources.


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. Groupoid Cafe: The Language of Space: slides, video.

5. Groupoid Cafe: Homotopy Type System with Strict Equality: homepage, 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).

4. Groupoid Infinity: Homotopy Type System with Strict Equality sources.


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 type systems and Groupoid Infinity mathematical library.

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

4. ERP.UNO — open source enterprise infrastructure (CA, DNS, LDAP, CRM).