Lukasz Czajka

Publication Activity (10 Years)

Years Active: 2011-2023
Publications (10 Years): 18

Top Topics

Lambda Calculus

Extended Abstract

Top Venues

Log. Methods Comput. Sci.

Publications

Ike Mulder, Lukasz Czajka, Robbert Krebbers
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Jan Bessai, Lukasz Czajka, Felix Laarmann, Jakob Rehof
Restricting Tree Grammars with Term Rewriting. FSCD (2022)
Lukasz Czajka
A new coinductive confluence proof for infinitary lambda calculus. Log. Methods Comput. Sci. 16 (1) (2020)
Lukasz Czajka
An operational interpretation of coinductive types. Log. Methods Comput. Sci. 16 (1) (2020)
Lukasz Czajka
Practical Proof Search for Coq by Type Inhabitation. IJCAR (2) (2020)
Lukasz Czajka, Cynthia Kop
Polymorphic Higher-Order Termination. FSCD (2019)
Lukasz Czajka, Cynthia Kop
Polymorphic Higher-order Termination. CoRR (2019)
Lukasz Czajka
First-Order Guarded Coinduction in Coq. ITP (2019)
Lukasz Czajka, Burak Ekici, Cezary Kaliszyk
Concrete Semantics with Coq and CoqHammer. CICM (2018)
Lukasz Czajka, Burak Ekici, Cezary Kaliszyk
Concrete Semantics with Coq and CoqHammer. CoRR (2018)
Lukasz Czajka
Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data. FSCD (2018)
Lukasz Czajka
An infinitary rewriting interpretation of coinductive types. CoRR (2018)
Lukasz Czajka
A new coinductive confluence proof for infinitary lambda-calculus. CoRR (2018)
Lukasz Czajka, Cezary Kaliszyk
Hammer for Coq: Automation for Dependent Type Theory. J. Autom. Reason. 61 (1-4) (2018)
Lukasz Czajka
Confluence of an Extension of Combinatory Logic by Boolean Constants. FSCD (2017)
Lukasz Czajka
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. CPP (2016)
Lukasz Czajka
A Shallow Embedding of Pure Type Systems into First-Order Logic. TYPES (2016)
Lukasz Czajka, Cezary Kaliszyk
Goal Translation for a Hammer for Coq (Extended Abstract). HaTT@IJCAR (2016)
Lukasz Czajka
Coinductive Techniques in Infinitary Lambda-Calculus. CoRR (2015)
Lukasz Czajka
On the equivalence of different presentations of Turner's bracket abstraction algorithm. CoRR (2015)
Lukasz Czajka
Confluence of nearly orthogonal infinitary term rewriting systems. RTA (2015)
Lukasz Czajka
A Coinductive Confluence Proof for Infinitary Lambda-Calculus. RTA-TLCA (2014)
Lukasz Czajka
Partiality and Recursion in Higher-Order Logic. FoSSaCS (2013)
Lukasz Czajka
Higher-order illative combinatory logic. J. Symb. Log. 78 (3) (2013)
Lukasz Czajka
Confluence of an extension of Combinatory Logic by Boolean Constants. CoRR (2013)
Lukasz Czajka
Higher-order illative combinatory logic CoRR (2012)
Lukasz Czajka
Partiality and Recursion in Higher-order Logic CoRR (2012)
Lukasz Czajka
A Semantic Approach to Illative Combinatory Logic. CSL (2011)