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