Refereed publications

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

PhD thesis

Łukasz Czajka: Semantic consistency proofs for systems of Illative Combinatory Logic, PhD thesis, 2015, slides, extended abstract: en, pl

Unpublished notes

  1. Łukasz Czajka: Coinduction: an elementary approach
  2. Łukasz Czajka: Needed rewriting
  3. Ł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.