Hammer for Coq: Automation for Dependent Type Theory Ł Czajka, C Kaliszyk Journal of Automated Reasoning 61 (1-4), 2018 | 164 | 2018 |
A coinductive confluence proof for infinitary lambda-calculus Ł Czajka International Conference on Rewriting Techniques and Applications, 164-178, 2014 | 26 | 2014 |
Practical proof search for coq by type inhabitation Ł Czajka Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris …, 2020 | 16 | 2020 |
Goal translation for a hammer for Coq Ł Czajka, C Kaliszyk HaTT 2016, 2016 | 13 | 2016 |
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions Ł Czajka Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 13 | 2016 |
Higher-order illative combinatory logic Ł Czajka The Journal of Symbolic Logic 78 (3), 837-872, 2013 | 13 | 2013 |
A new coinductive confluence proof for infinitary lambda calculus Ł Czajka Logical Methods in Computer Science 16 (1), 2020 | 12 | 2020 |
Coinductive techniques in infinitary lambda-calculus Ł Czajka ArXiv e-prints, 2015 | 10 | 2015 |
A semantic approach to illative combinatory logic L Czajka Computer Science Logic (CSL'11)-25th International Workshop/20th Annual …, 2011 | 10 | 2011 |
A shallow embedding of pure type systems into first-order logic L Czajka 22nd International Conference on Types for Proofs and Programs (TYPES 2016), 2018 | 7 | 2018 |
Coinduction: an elementary approach Ł Czajka arXiv preprint arXiv:1501.04354, 2015 | 6 | 2015 |
Confluence of nearly orthogonal infinitary term rewriting systems L Czajka 26th International Conference on Rewriting Techniques and Applications (RTA …, 2015 | 6 | 2015 |
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic I Mulder, Ł Czajka, R Krebbers Proceedings of the ACM on Programming Languages 7 (PLDI), 1340-1364, 2023 | 4 | 2023 |
Concrete semantics with Coq and CoqHammer Ł Czajka, B Ekici, C Kaliszyk Intelligent Computer Mathematics: 11th International Conference, CICM 2018 …, 2018 | 4 | 2018 |
Restricting Tree Grammars with Term Rewriting J Bessai, L Czajka, F Laarmann, J Rehof 7th International Conference on Formal Structures for Computation and …, 2022 | 3 | 2022 |
Partiality and recursion in higher-order logic Ł Czajka International Conference on Foundations of Software Science and …, 2013 | 3 | 2013 |
Term rewriting characterisation of LOGSPACE for finite and infinite data L Czajka 3rd International Conference on Formal Structures for Computation and …, 2018 | 2 | 2018 |
On the equivalence of different presentations of Turner's bracket abstraction algorithm Ł Czajka arXiv preprint arXiv:1510.03794, 2015 | 2 | 2015 |
Semantic consistency proofs for systems of illative combinatory logic Ł Czajka Ph. D. Thesis, University of Warsaw, 2015 | 2 | 2015 |
Parametricity and syntactic logical relations in System F Ł Czajka | | 2022 |