Lukasz Czajka

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