Hello! My name is Łukasz Czajka. I’m a compiler engineer and a programming language designer. I used to work full-time in academia doing research in broadly understood computational logic, which I still pursue as a hobby.

Interests

Currently, I work on the design and implementation of the functional programming language Juvix.

I’m interested in type theory, functional programming, theory and implementation of programming languages, and deductive program verification. I’ve done some teaching related to these topics.

My principal research interests include automation for proof assistants and proof search in non-classical logics. I’m the main developer and maintainer of the CoqHammer automated reasoning system for Coq. I wrote a Coq plugin to help with proofs by coinduction. I’ve been working on proof search in dependent type theory and intuitionistic logic, and on improving automation for disjunctive formulas in IRIS.

During my past academic career, I published some theoretical papers at the border of type theory and term rewriting. I’ve also worked on the infinitary lambda calculus and combinatory logic. Some of this research earned references in the new monograph Lambda Calculus Satellite by Barendregt and Manzonetto.

I have a solid background in proof assistants, compiler construction, design and implementation of programming languages, low-level systems programming, and implementation of efficient algorithms and data structures. See also my software projects.

Bio

I received my Ph.D. from the University of Warsaw under supervision of Paweł Urzyczyn. Then I was a postdoc in Innsbruck where I developed CoqHammer with Cezary Kaliszyk. After that I received a Marie Curie Individual Fellowship to move to Copenhagen and work on an infinitary rewriting interpretation of coinductive types. Afterwards, I spent several years as a researcher at the Technical University of Dortmund. Now I work in the industry.

Contact

Email (still valid, but I’m not at MIMUW anymore): lukaszcz at mimuw edu pl