Refereed publications

  1. Ike Mulder, Łukasz Czajka, Robbert Krebbers: Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic, PLDI 2023
  2. Jan Bessai, Łukasz Czajka, Felix Laarmann, Jakob Rehof: Restricting Tree Grammars with Term Rewriting, FSCD 2022
  3. Łukasz Czajka: Practical proof search for Coq by type inhabitation, IJCAR 2020, (evaluations) (slides)
  4. Łukasz Czajka: A new coinductive confluence proof for infinitary lambda-calculus, Logical Methods in Computer Science, Volume 16, Issue 1 (2020), (Coq formalisation)
  5. Łukasz Czajka: An operational interpretation of coinductive types, Logical Methods in Computer Science, Volume 16, Issue 1 (2020)
  6. Łukasz Czajka: First-order guarded coinduction in Coq, ITP 2019 (slides) (Coq plugin)
  7. Łukasz Czajka, Cynthia Kop: Polymorphic Higher-order Termination, FSCD 2019 (slides)
  8. Łukasz Czajka, Burak Ekici, Cezary Kaliszyk: Concrete Semantics with Coq and CoqHammer, CICM 2018
  9. Łukasz Czajka: Term rewriting characterisation of LOGSPACE for finite and infinite data, FSCD 2018 (slides)
  10. Ł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)
  11. Łukasz Czajka: Confluence of an extension of Combinatory Logic by Boolean constants, FSCD 2017 (solves RTA open problem 15) (Coq formalisation) (slides)
  12. Łukasz Czajka: A Shallow Embedding of Pure Type Systems into First-Order Logic, TYPES 2016, LIPIcs vol. 97
  13. Łukasz Czajka: Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions, CPP 2016
  14. Łukasz Czajka: Confluence of nearly orthogonal infinitary term rewriting systems, RTA 2015
  15. Łukasz Czajka: A Coinductive Confluence Proof for Infinitary Lambda-Calculus, RTA-TLCA 2014 (best student paper award) (slides)
  16. Łukasz Czajka: Partiality and recursion in higher-order logic, FoSSaCS 2013 (slides)
  17. Łukasz Czajka: Higher-order illative combinatory logic, Journal of Symbolic Logic, Volume 78, Issue 3 (2013)
  18. Łukasz Czajka: A semantic approach to illative combinatory logic, CSL 2011

Workshops (selected)

  1. Łukasz Czajka, Cezary Kaliszyk: CoqHammer: A General-Purpose Automated Reasoning Tool for Coq, EUTYPES 2018, invited talk
  2. Łukasz Czajka, Cezary Kaliszyk: CoqHammer: Strong Automation for Program Verification, CoqPL 2018, keynote (slides)
  3. Łukasz Czajka, Cezary Kaliszyk: Goal Translation for a Hammer for Coq (Extended Abstract), HaTT 2016
  4. Łukasz Czajka, Cezary Kaliszyk: Components of a Hammer for Type Theory: Coq Goal Translation and Reconstruction, TYPES 2016 (slides)

Technical reports

  1. Łukasz Czajka, The Core language of Juvix, ART, 2023
  2. Ł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

  1. Łukasz Czajka: Parametricity and syntactic logical relations in System F
  2. Łukasz Czajka: Needed rewriting
  3. Łukasz Czajka: Coinduction: an elementary approach
  4. Ł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.