Hi! Welcome to my personal page. I love systems programming and building simple, robust, and performant software. I used to do a bit of type theory, programming languages research, robotics, and gamedev. Currently, I work at a trading startup where we’re building a systematic trading platform in Rust from scratch.
Projects
Some older projects I had fun building (even though they don’t reflect my current skills).
2023
-
Lincheck
A library for testing concurrent data structures for linearizability. It is inspired by Lincheck for Kotlin and is built on top of loom, a model-checker for concurrency.
-
GQL in Coq
Mechanized formalization of the core subset of GQL in Coq, and a proof of correctness of the key implementation details of two reference databases: Neo4j and RedisGraph.
2022
-
MTT Lang
Interpreter for a functional programming language with Modal Type Theory which supports user-defined algebraic data types and pattern-matching.
-
Simple Type Checker
Type checker for Church-style Polymorphic Lambda Calculus (System F).
2021
-
High Shift Engine
Data-oriented game engine designed for maintaining large dynamically changing structures of entities.
-
Huffman Archiver
Archiver with canonical Huffman codes designed for fast and memory efficient encoding and decoding of big files.
2020
-
Bachero
2d game engine based on SDL2 with ECS architecture and a custom physics engine.
-
Text Index
A tool, built with clean architecture principles in mind, that provides fast text indexing and querying.
2019
-
Path Builder
The service for solving an instance of traveling salesman problem. The task is to find the optimal route through all the given places while respecting all the timing requirements.
-
AIst
The software for an autonomous robot based on NVidia Jetson 2. The robot can move along the black line, and recognize signs and traffic lights. The behavior is controlled by a stack-based state machine.