Papers of Łukasz Czajka

Refereed publications (journals and refereed conference proceedings)

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

Short notes, submitted and unpublished work

  1. Łukasz Czajka: A new coinductive confluence proof for infinitary lambda-calculus, submitted (Coq formalisation)
  2. Łukasz Czajka: An infinitary rewriting interpretation of coinductive types, submitted
  3. Łukasz Czajka: Coinduction: an elementary approach
  4. Łukasz Czajka: Needed rewriting
  5. Ł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.


back to main page Last updated 11 September 2019 by Łukasz Czajka