5HT

COURSES

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).

PUBLICATIONS

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.

TALKS

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.

PURE

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).

GENERAL

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)

DOMAIN

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).

DATA

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).

SITES

These are my open-source projects.

1. Longchen Nyingthig: site.

2. Groupoid Infinity: site.

3. N2O Ecosystem: site.