Papers
Refereed publications
- Ike Mulder, Łukasz Czajka, Robbert Krebbers: Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic, PLDI 2023
- Jan Bessai, Łukasz Czajka, Felix Laarmann, Jakob Rehof: Restricting Tree Grammars with Term Rewriting, FSCD 2022
- Łukasz Czajka: Practical proof search for Coq by type inhabitation, IJCAR 2020, (evaluations) (slides)
- Łukasz Czajka: A new coinductive confluence proof for infinitary lambda-calculus, Logical Methods in Computer Science, Volume 16, Issue 1 (2020), (Coq formalisation)
- Łukasz Czajka: An operational interpretation of coinductive types, Logical Methods in Computer Science, Volume 16, Issue 1 (2020)
- Łukasz Czajka: First-order guarded coinduction in Coq, ITP 2019 (slides) (Coq plugin)
- Łukasz Czajka, Cynthia Kop: Polymorphic Higher-order Termination, FSCD 2019 (slides)
- Łukasz Czajka, Burak Ekici, Cezary Kaliszyk: Concrete Semantics with Coq and CoqHammer, CICM 2018
- Łukasz Czajka: Term rewriting characterisation of LOGSPACE for finite and infinite data, FSCD 2018 (slides)
- Łukasz Czajka, Cezary Kaliszyk: Hammer for Coq: Automation for Dependent Type Theory, Journal of Automated Reasoning, Volume 61, Issue 1-4 (2018), (CoqHammer webpage) (CoqHammer GitHub repository)
- Łukasz Czajka: Confluence of an extension of Combinatory Logic by Boolean constants, FSCD 2017 (solves RTA open problem 15) (Coq formalisation) (slides)
- Łukasz Czajka: A Shallow Embedding of Pure Type Systems into First-Order Logic, TYPES 2016, LIPIcs vol. 97
- Łukasz Czajka: Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions, CPP 2016
- Łukasz Czajka: Confluence of nearly orthogonal infinitary term rewriting systems, RTA 2015
- Łukasz Czajka: A Coinductive Confluence Proof for Infinitary Lambda-Calculus, RTA-TLCA 2014 (best student paper award) (slides)
- Łukasz Czajka: Partiality and recursion in higher-order logic, FoSSaCS 2013 (slides)
- Łukasz Czajka: Higher-order illative combinatory logic, Journal of Symbolic Logic, Volume 78, Issue 3 (2013)
- Łukasz Czajka: A semantic approach to illative combinatory logic, CSL 2011
Workshops (selected)
- Łukasz Czajka, Cezary Kaliszyk: CoqHammer: A General-Purpose Automated Reasoning Tool for Coq, EUTYPES 2018, invited talk
- Łukasz Czajka, Cezary Kaliszyk: CoqHammer: Strong Automation for Program Verification, CoqPL 2018, keynote (slides)
- Łukasz Czajka, Cezary Kaliszyk: Goal Translation for a Hammer for Coq (Extended Abstract), HaTT 2016
- Łukasz Czajka, Cezary Kaliszyk: Components of a Hammer for Type Theory: Coq Goal Translation and Reconstruction, TYPES 2016 (slides)
Technical reports
- Łukasz Czajka, Compiling Juvix to Cairo Assembly, ART, 2024
- Łukasz Czajka, The Core language of Juvix, ART, 2023
- Łukasz Czajka, Juvix to VampIR pipeline, ART, 2023
PhD thesis
Łukasz Czajka: Semantic consistency proofs for systems of Illative Combinatory Logic, PhD thesis, 2015, slides, extended abstract: en, pl
Related: HCPL implementation
Unpublished notes
- Łukasz Czajka: Parametricity and syntactic logical relations in System F
- Łukasz Czajka: Needed rewriting
- Łukasz Czajka: Coinduction: an elementary approach
- Łukasz Czajka: On the equivalence of different presentations of Turner’s bracket abstraction algorithm
Links to arxiv point to short notes, preprints or extended versions.