Hi! Welcome to my personal page. I am interested in building reliable and highly performant systems by leveraging formal methods and systems programming languages. I am also interested in functional programming and type theory. I was doing some robotics and gamedev in the past.
Projects
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.