Papers of Łukasz Czajka

Refereed publications (journals and refereed conference proceedings)

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

Short notes, submitted and unpublished work

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.