Hello! My name is Łukasz Czajka. I’m a researcher in broadly understood computational logic.


Most of my theoretical publications fall at the border of type theory and term rewriting. I’ve also worked on the infinitary lambda calculus and combinatory logic.

I’m interested in automation for proof assitants 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.

Recently, I’ve been working on proof search in dependent type theory and intuitionistic logic, and on improving automation for disjunctive formulas in IRIS.

Outside of my research, I maintain a general interest in functional programming, theory and implementation of programming languages, and deductive program verification. I’ve done some teaching related to these topics.

In the past, during my student years and earlier, in addition to my ongoing interest in logic and theoretical computer science, I also engaged in compiler construction, design and implementation of programming languages, low-level programming, and implementation of efficient algorithms and data structures. I still remember much from that. See also my software projects.


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. Now I am at the Technical University of Dortmund.


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