A Semantic Approach to Illative Combinatory Logic. - Lukasz Czajka 001 (CSL, 2011)

Partiality and Recursion in Higher-Order Logic. - Lukasz Czajka 001 (FoSSaCS, 2013)

Higher-order illative combinatory logic. - Lukasz Czajka 001 (J. Symb. Log., 2013)

A Coinductive Confluence Proof for Infinitary Lambda-Calculus. - Lukasz Czajka 001 (RTA-TLCA, 2014)

Confluence of nearly orthogonal infinitary term rewriting systems. - Lukasz Czajka 001 (RTA, 2015)

Coinductive Techniques in Infinitary Lambda-Calculus. - Lukasz Czajka 001 (CoRR, 2015)

On the equivalence of different presentations of Turner's bracket abstraction algorithm. - Lukasz Czajka 001 (CoRR, 2015)

Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. - Lukasz Czajka 001 (CPP, 2016)

A Shallow Embedding of Pure Type Systems into First-Order Logic. - Lukasz Czajka 001 (TYPES, 2016)

Goal Translation for a Hammer for Coq (Extended Abstract). - Lukasz Czajka 001; Cezary Kaliszyk (HaTT@IJCAR, 2016)

Confluence of an Extension of Combinatory Logic by Boolean Constants. - Lukasz Czajka 001 (FSCD, 2017)

Concrete Semantics with Coq and CoqHammer. - Lukasz Czajka 001; Burak Ekici; Cezary Kaliszyk (CICM, 2018)

Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data. - Lukasz Czajka 001 (FSCD, 2018)

An infinitary rewriting interpretation of coinductive types. - Lukasz Czajka 001 (CoRR, 2018)

Hammer for Coq: Automation for Dependent Type Theory. - Lukasz Czajka 001; Cezary Kaliszyk (J. Autom. Reason., 2018)

First-Order Guarded Coinduction in Coq. - Lukasz Czajka 001 (ITP, 2019)

Polymorphic Higher-Order Termination. - Lukasz Czajka 001; Cynthia Kop (FSCD, 2019)

Practical Proof Search for Coq by Type Inhabitation. - Lukasz Czajka 001 (IJCAR (2), 2020)

An operational interpretation of coinductive types. - Lukasz Czajka 001 (Log. Methods Comput. Sci., 2020)

A new coinductive confluence proof for infinitary lambda calculus. - Lukasz Czajka 001 (Log. Methods Comput. Sci., 2020)

Restricting Tree Grammars with Term Rewriting. - Jan Bessai; Lukasz Czajka 001; Felix Laarmann; Jakob Rehof (FSCD, 2022)

Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. - Ike Mulder; Lukasz Czajka 001; Robbert Krebbers (Proc. ACM Program. Lang., 2023)