I grew up in Nowa Ruda, a small town in south-western Poland. I taught myself programming and system administration at a very young age. (I was quite a nerd!) I have studied computer science at the University of Wrocław. My master's thesis, supervised by Jerzy Marcinkowski, involved creating an interactive theorem prover for teaching logic to university freshmen and high school students. My PhD thesis, supervised by Dariusz Biernacki and Jerzy Marcinkowski, is a study of the Danvy and Filinski's shift0 control operator.
My primary research interest is programming languages, including semantics, type systems and implementation. I'm also interested in formal logic and computer-assisted theorem proving.
My non-research interests include photography, electronics and (tandem) cycling.
Easyprove: a tool for teaching precise reasoning
Tools for Teaching Logic (TTL'15)
Subtyping Delimited Continuations
To be published in Higher-Order and Symbolic Computation
Axiomatizing Subtyped Delimited Continuations
Computer Science Logic (CSL'13)
Proving Termination of Evaluation for System F with Control Operators
Control Operators and their Semantics (COS'13)
A Dynamic Interpretation of the CPS Hierarchy
Asian Symposium on Programming Languages and Systems (APLAS'12)
Subtyping delimited continuations
International Conference on Functional Programming (ICFP'11)
Undergrad projects and other achievements
Here are some useful, interesting or amusing things I did before graduating.
During M.sc. studies
- A simple database engine for a subset of XQuery. Uses BerkeleyDB for storage, does some simple optimizations. Written in Haskell, uses lazy evaluation heavily.
- A distributed system for judging solutions in programming contests. Written mostly in Erlang, a small part is written in C. Runs on the Computer Science Portal of Wroclaw (Wrocławski Portal Informatyczny).
- A note about existence of solutions of recursive equations on domains, with (almost working) Haskell implementation. In Polish, lots of category theory inside. Written for Semantics of programming languages (Semantyki języków programowania) course.
- Generic bananas, lenses, envelopes and barbed wire (the ones from here) in Haskell. Inspired by category theory. Co-barbed wire included! (Literate Haskell, in Polish.)
- LOL - a compiler for a simple lazy dependently-typed language. Targets LLVM. Written for Methods of translation (Metody translacji) course. Not particularly complete, or efficient - it uses an old G-machine design - but it helped me understand compiling lazy languages.
- An arrow parser library in Haskell. Non-backtracking, allows for incremental parsing. Used in LOL.
- A formal proof of correctness of the unification algorithm, in HOL. Written with Maciej Piróg, Łukasz Stafiniak and Piotr Witkowski for the Interactive Proof Systems seminar. I have some slides about the proof.
- A talk (in Polish) about functional reactive programming.
- A talk (in Polish) about the Erlang programming language. Just an introduction, no advanced stuff like the OTP, Mnesia and the like.
- A talk (in Polish) about the Haskell implementation of Software Transactional Memory. Given on ZOSIA 2007 student conference.
- A talk (in Polish) about esoteric programming languages and compiling things to them.
- lisp2unlambda - compiles a Lisp-like language to Unlambda.
- An article (in Polish) about microkernel-based operating systems. Written for the Operating systems (Systemy operacyjne) course.
- An article (in Polish) about historical programming languages: Konrad Zuse's Plankalkül, Fortran, Algol and LISP. Written for the History of computing (Historia rachowania) course.
- Wraith - parser generator in a macro for Nemerle. Bootstrapped - uses itself to parse grammar definitions.
- A talk (in Polish) about the L4Ka microkernel. I liked the concept back then, now I think that programming language-secured systems like Microsoft's Singularity (and House OS, written in Haskell) are the way to go.
- I took part in several programming contests: ACM ICPC, MWPZ, DZPZ, Potyczki Algorytmiczne and others. I never was good enough to win anything significant, but I've managed to get to the CEPC twice and be near the top ten.
In high school and before
- Several articles for Linux+ and Software 2.0 magazines: one about basics of using Linux (i was something of a Linux zealot back then), one about Boost C++ libraries, and one about the Boost.Spirit parser library. I didn't know Haskell then, so I didn't notice Spirit is just a lame Parsec.
- Tanuki Anime and Tanuki Manga - simple database-driven web sites. As of today, they are the most popular sites in Poland about Japanese animation and comics. I'm not too interested in this stuff today... Maybe I've just grown up.
- High-Level Brainfuck - a compiler from a simple imperative language to Brainfuck. Written in Python. Warning: lots of brackets and +/- signs.
- Bf2llvm - a Brainfuck to LLVM compiler. Makes Brainfuck programs almost run fast!
- Llfunge - a Befunge JIT compiler using LLVM. Almost correct - it disallows program mutation.
- 31337 recoder - a program for encoding text to binary, hexadecimal, ROT13, Morse alphabet and so on. A necessity in every 1337 |-|4><0Rz toolbox.
- LinuxZone at linux.gery.pl, a tutorial website about using Linux.
- TilkIRClog (what a thought out name!) - a simple IRC bot with logging and mailing capability. Written when I was using a modem Internet connection. I planned a more modular version, but it was never completed.