Lukasz Czajka

According to our database, Lukasz Czajka authored at least 22 papers between 2011 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic.

Ike Mulder, Lukasz Czajka, Robbert Krebbers

Proc. ACM Program. Lang., 2023

2022

Restricting Tree Grammars with Term Rewriting.

Jan Bessai, Lukasz Czajka, Felix Laarmann, Jakob Rehof

Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

2020

A new coinductive confluence proof for infinitary lambda calculus.

Lukasz Czajka

Log. Methods Comput. Sci., 2020

An operational interpretation of coinductive types.

Lukasz Czajka

Log. Methods Comput. Sci., 2020

Practical Proof Search for Coq by Type Inhabitation.

Lukasz Czajka

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Polymorphic Higher-Order Termination.

Lukasz Czajka, Cynthia Kop

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

First-Order Guarded Coinduction in Coq.

Lukasz Czajka

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018

Hammer for Coq: Automation for Dependent Type Theory.

Lukasz Czajka, Cezary Kaliszyk

J. Autom. Reason., 2018

An infinitary rewriting interpretation of coinductive types.

Lukasz Czajka

CoRR, 2018

Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data.

Lukasz Czajka

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

Concrete Semantics with Coq and CoqHammer.

Lukasz Czajka, Burak Ekici, Cezary Kaliszyk

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

2017

Confluence of an Extension of Combinatory Logic by Boolean Constants.

Lukasz Czajka

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

2016

Goal Translation for a Hammer for Coq (Extended Abstract).

Lukasz Czajka, Cezary Kaliszyk

Proceedings of the Proceedings First International Workshop on Hammers for Type Theories, 2016

A Shallow Embedding of Pure Type Systems into First-Order Logic.

Lukasz Czajka

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions.

Lukasz Czajka

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015

On the equivalence of different presentations of Turner's bracket abstraction algorithm.

Lukasz Czajka

CoRR, 2015

Coinductive Techniques in Infinitary Lambda-Calculus.

Lukasz Czajka

CoRR, 2015

Confluence of nearly orthogonal infinitary term rewriting systems.

Lukasz Czajka

Proceedings of the 26th International Conference on Rewriting Techniques and Applications, 2015

2014

A Coinductive Confluence Proof for Infinitary Lambda-Calculus.

Lukasz Czajka

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

2013

Higher-order illative combinatory logic.

Lukasz Czajka

J. Symb. Log., 2013

Partiality and Recursion in Higher-Order Logic.

Lukasz Czajka

Proceedings of the Foundations of Software Science and Computation Structures, 2013

2011

A Semantic Approach to Illative Combinatory Logic.

Lukasz Czajka

Proceedings of the Computer Science Logic, 2011