Adress: Building 14 (Applied Mathematics),
Polytechnichna str. 14-A, Kyiv, Ukraine, 03056.
I am a Ph.D. student in the Applied Mathematics Faculty at National Technical University of Ukraine «Igor Sikorsky Kyiv Polytechnic Institute». I received MSc at same place with «Business Process Engine: Theory and Implementation» work, which was later adopted to production as BPE library in PrivatBank, one of the biggest bank in Eastern Europe. Before I received BSc at same place with «PL/1: Design and Implementation for .NET CLR». All my academic works are done under supervision of Pavlo Maslianko.
My current research interests focus on cubical type checkers and formalization of mathematics. I do love code in cubicaltt, but respect other HoTT provers, like yacctt, RedPRL, agda --cubical. Also I love to create programming languages.
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
1. MLTT Intro and Categorical Semantics of Inductive Types: video
3. Cubical Live Coding (MLTT Rules): video
4. f(cafe): The Language of Space: slides
1. Groupoid Infinity: The Language of Space: sources. (Mathematical Components).
2. OM: Consistent PTS with Universes for Erlang: sources. (Academic, Educational, Teaching).
1. O: L1 sized byte code interpreter with AVX Vectorization in Rust: sources. (Prototype).
2. Joxa modification for Erlang AST compilation: sources. (Toy)
3. Lazy ML with Process Calculus in C: sources. (Toy)
5. Lisp for .NET: sources. (International Land Systems, Inc. Production).
6. PL/1 .NET: sources. (BSc)
3. UPL for Erlang: sources (Experimental).
1. Longchen Nyingthig: site
2. Groupoid Infinity: site
3. N2O Ecosystem: site
4. Operating System with immutable CAS queues and K flavored Programming Language: site