• Functional programming
• Compiler construction
• Type theory
• Blockchain
• Formal verification

• Advanced: Haskell, Erlang, Coq
• Semi-advanced: C#, Rust
• Intermediate: Python, Prolog

• Mothertongue: Polish
• Fluent: English
• Communicative: German

• Researching methods for verification of distributed systems
• Teaching assistance in computer science master's courses

• Developing a compiler for a smart contract language
• Developing tooling for smart contract development
• Developing a virtual machine for smart contracts
• Conducting technical interviews and onboarding new members

• Developed the server behind Business Central 365
• Maintained site reliability

• Introduced a new booking infra for the company's services
• Introduced Elm to the codebase

• Research project: "Hyben - Hybrid Verification of Heterogeneous Message-Passing Applications"
• Formalised methods of distributed deadlock detection via black-box monitors
• Mechanised theoretical results in Rocq
• Implemented tools for deadlock detection in gen_server-based systems: DDMon and DDTrace

Master's degree in computer science.

• Thesis: Liquid types for verification of smart contracts
• Grade: Very Good (5 in a 2–5 scale)

Student exchange programme

Bachelor's degree in computer science

• Thesis: Variational autoencoder for collaborative filtering - implementation and performance optimization
• Grade: Good (4 in a 2–5 scale)

• ddmon — A prototype tool for distributed deadlock detection in Erlang/Elixir systems based on the gen_server behaviour. Implemented as black-box proxy monitors. Works as a drop-in replacement for the gen_server module.
• ddtrace — Another distributed deadlock detecting tool for generic servers in Erlang, but this time based on observing monitors that do not require any intervention in the code of the monitored process. Instead, uses built-in trace facility to make deadlock verdicts based solely on incoming and outgoing communication.
• dlstalk — Fully mechanised formalisation of a deadlock detecting algorithm via proxy monitors. Specifies syntax and semantics of monitored and unmonitored services and networks and proves transparency and preciseness of deadlock verdicts. ddmon is the implementation of this model.

• aesophia — I developed the Sophia smart contract language for the æternity blockchain.
• aerepl — I designed and implemented a Read-Eval-Print Loop and debugger for the Sophia language.
• aerepl-web — Web interface for æREPL implemented by me.
• aeserialization-rust — I rewrote core components of the æternity blockchain in Rust.
• tree-sitter-aesophia — I implemented a Tree-sitter grammar for æternity's smart contract language.
• erlscripten — I took key part in the erlscripten project, which aims to port Erlang applications to the frontend of web applications by transpiling it into PureScript.
• erlscripten/purescript — For the erlscripten project I did a lot of tinkering in the source generator and optimizer of PureScript's compiler. My work resulted in a few contributions to the original project:
  • #4006 — I identified and fixed a performance issue in one of PureScript's AST transformations.
  • #3968 — I proposed changes to how tail-call optimizations are triggered (unmerged).

• radlang — An interpreter of a Haskell-like language. Supports type classes, full type inference, higher kinded types, for notation for monads and lazy evaluation.
• latte — An x86 compiler for a Java-like OOP language. Implements class inheritance, polymorphism via virtual methods and some simple optimization techniques.
• satisfaction — A SAT solver implementing CDCL and DPLL algorithms written in Rust as an assessment task for courses at LMU.
• VAE-CF — Bachelor's thesis project. A variational autoencoder for collaborative filtering written in Tensorflow. Created in cooperation with NVIDIA Corporation to optimize it for their hardware and infrastructure.
• tftp-client-coq — A TFTP client written in Coq/OCaml. Provides proofs for compliance with the RFC standard.
• Tiny-Semantics — A simple CPS-styled interpreter of an imperative language written in Haskell.
• instant-compiler — A calculator-like language compiler that targets LLVM and JVM.

• i3hloc — A customizable, parallelized scheduler for the i3status status bar for i3 WM. Written in Haskell.
• fizzbuzz-coq — A super defensive joke implementation of the Fizz Buzz problem written as a sophisticated proposal to the state-of-the-art implementation. Written in Coq to prove correctness of every step of the algorithm. Obfuscation warning.
• blockchain-toy — A simple centralized blockchain implementation written in Haskell.
• Iris — I provided the Iris Mopidy frontend with Polish localization.