5HT

АФІЛІАЦІЇ

1. Релігійна організація «Лонгчен Нінгтік Україна» longchenpa.guru, директор.

2. Інститут формальної математики «Групоїд Інфініті» groupoid.space, дослідник.

3. Видавництво «Аксіосис» axiosis.top, головний редактор.

4. Державна ІТ-компанія «ІНФОТЕХ» infotech.gov.ua, провідний інженер-програміст.

КНИГИ

1. ISBN: 978-1-62540-054-3 Ньондро

2. ISBN: 978-617-8027-08-7 Формальна система #1

3. ISBN: 978-617-8027-10-0 Безумний монах

4. ISBN: 978-617-8027-27-8 Топовий програміст

5. ISBN: 978-617-8027-23-0 Державна система #1

6. ISBN: 978-617-8027-07-0 Ідея Нації

7. ISBN: 978-617-8027-07-1 Посібник МІА:СЕД

8. ISBN: 978-617-8027-23-1 Формальна філософія

КУРСИ

1. Вступ до HoTT 2018–2019 — intro, video (3 hr).

2. Ерланг курси 2013–2014 — video (12 hrs).

ВИСТУПИ

1. Категорна семантика індуктивних типів відео. НАН України.

2. Презентація cubicaltt by Anders Mörtberg et all: відео 1, відео 2. НАН України.

3. MLTT правила, жива сесія: відео. НАН України.

4. Groupoid Cafe: The Language of Space: слайди, відео. Інтетікс.

5. Groupoid Cafe: Homotopy Type System with Strict Equality: сайт, відео. ДП «ІНФОТЕХ».

СКОПУС

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

4. Issue III: Homotopy Type Theory. PDF.

5. Issue VIII: Formal Topos on Category of Sets. PDF.

6. Mathematical Components. TeX.

7. Modal Homotopy Type System. сайт, PDF, код.

8. Фреймворк для підприємств ISO 20922. сайт.

7. Система управління процесами ISO 19510. сайт.

8. Одноаксіоматична система верифікації ПЗ. PDF.

9. Мінімальна система для вбудовування MLTT. PDF.

10. Мова для квантових комп'ютерів PLQ. PDF.

ЧИСТІ МОВИ

Мої чисті мови програмування.

1. Henk: Pure Type System for Erlang. код.

3. The Cubical Base Library. сайт, код. (cubicaltt).

5. Математична бібліотека мови Anders Groupoid Infinity.

4. Anders: Homotopy Type System with Strict Equality. код.

ЗАГАЛЬНІ МОВИ

Мої спроби побудови рантаймів та мов загального використання, в основному спеціалізуюся на інтерпретаторах та гомотопічних логічних системах.

1. O: APL інтерпретатор з AVX векторизацією та L1-кеш футпрінтом рантайма: код. (Прототип, Виробництво).

2. Lazy ML інтерпретатор з численням процесів Мілнера: код. (Іграшка).

3. Io інтерпретатор in C#: код. (Експеримент, listed at iolanguage.org).

4. Lisp інтерпретатор in C#: код. (Виробництво, International Land Systems, Inc.).

5. PL/1 компілятор in C#: код. (BSc).

СПЕЦІАЛІЗОВАНІ МОВИ

Мої мови спеціального призначення, які використовуються в ПриватБанк та МВС.

1. BPE: система управління процесами для Erlang: site, sources (MSc, Production).

2. UPL: декларативна мова тарифних моделей для Erlang: sources (Experimental).

3. FormalTalk: декларативна мова з обмеженими імперативними властивостями: sources (Experimental).

4. ASN.1: компілятор в мову Swift 5.8: sources (WIP).

МОВИ ДЛЯ ДАНИХ

Мої мови для даних, які використовуються в стартапах Америки, Європи та Азії.

1. CR: Реалізація BFT шляхом ланцюжкової реплікації для Erlang: article, sources. (Experimental).

2. KVS: Мова управління курсорами для Erlang: site, sources (Production).

САЙТИ

Кожен з моїх сайтів відвудує та читає від 2 то 7 тис унікальних хостів на місяць.

1. Longchen Nyingthig — академічні дослідження тибетської релігійної поезії.

2. Інститут формальної математики Групоїд Інфініті.

3. N2O.DEV — телекомунікаційний фреймворк Synrc Україна.

4. ERP.UNO — система управління державними підприємствами.

5. Математична бібліотека Groupoid Infinity.