| 2026 | FSCD | Polymorphism Meets DHOL. | Rhea Ranalter, Florian Rabe, Cezary Kaliszyk |
| 2025 | IJCAI | Automated Strategy Invention for Confluence of Term Rewrite Systems. | Liao Zhang, Fabian Mitterwallner, Jan Jakubuv, Cezary Kaliszyk |
| 2024 | IJCAR | Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic. | Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk |
| 2024 | ITP | Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. | Karol Pak, Cezary Kaliszyk |
| 2024 | LPAR | Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery. | Kristina Aleksandrova, Jan Jakubuv, Cezary Kaliszyk |
| 2024 | LPAR | Experiments with Choice in Dependently-Typed Higher-Order Logic. | Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk |
| 2023 | CPP | Improved Assistance for Interactive Proof (Keynote). | Cezary Kaliszyk |
| 2023 | ITP | MizAR 60 for Mizar 50. | Jan Jakubuv, Karel Chvalovsk, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsk, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban |
| 2023 | LPAR | Experiments on Infinite Model Finding in SMT Solving. | Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk |
| 2022 | CADE | Lash 1.0 (System Description). | Chad E. Brown, Cezary Kaliszyk |
| 2022 | CAV | Proofgold: Blockchain for Formal Methods. | Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban |
| 2022 | FlAIRS | Adversarial Learning to Reason in an Arbitrary Logic. | Stanislaw J. Purgal, Cezary Kaliszyk |
| 2022 | IJCAI | Learning Higher-Order Logic Programs From Failures. | Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk |
| 2022 | ITP | The Isabelle ENIGMA. | Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsk, Jelle Piepenbrock, Josef Urban |
| 2022 | ITP | Formalizing a Diophantine Representation of the Set of Prime Numbers. | Karol Pak, Cezary Kaliszyk |
| 2021 | ICLR | Disambiguating Symbolic Expressions in Informal Documents. | Dennis Mller, Cezary Kaliszyk |
| 2021 | TABLEAUX | Towards Finding Longer Proofs. | Zsolt Zombori, Adrin Csiszrik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban |
| 2020 | CPP | Exploration of neural machine translation in autoformalization of mathematics in Mizar. | Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban |
| 2020 | ECAI | Property Invariant Embedding for Automated Reasoning. | Miroslav Olsk, Cezary Kaliszyk, Josef Urban |
| 2019 | CADE | GRUNGE: A Grand Unified ATP Challenge. | Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban |
| 2019 | ITP | Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. | Chad E. Brown, Cezary Kaliszyk, Karol Pak |
| 2019 | ITP | Declarative Proof Translation (Short Paper). | Cezary Kaliszyk, Karol Pak |
| 2019 | TABLEAUX | Certification of Nonclausal Connection Tableaux Proofs. | Michael Frber, Cezary Kaliszyk |
| 2018 | CPP | Formal microeconomic foundations and the first welfare theorem. | Cezary Kaliszyk, Julian Parsert |
| 2018 | ITP | Towards Formal Foundations for Game Theory. | Julian Parsert, Cezary Kaliszyk |
| 2017 | CADE | Monte Carlo Tableau Proof Search. | Michael Frber, Cezary Kaliszyk, Josef Urban |
| 2017 | FedCSIS | Progress in the Independent Certification of Mizar Mathematical Library in Isabelle. | Cezary Kaliszyk, Karol Pak |
| 2017 | ICLR | HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. | Cezary Kaliszyk, Franois Chollet, Christian Szegedy |
| 2017 | ITP | Automating Formalization by Statistical and Semantic Parsing of Mathematics. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2017 | LPAR | TacticToe: Learning to Reason with HOL4 Tactics. | Thibault Gauthier, Cezary Kaliszyk, Josef Urban |
| 2017 | LPAR | Deep Network Guided Proof Search. | Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk |
| 2017 | SYNASC | System Description: Statistical Parsing of Informalized Mizar Formulas. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2016 | CADE | No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions. | Michael Frber, Cezary Kaliszyk |
| 2016 | CADE | TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. | Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe |
| 2016 | CIKM | Initial Experiments with Statistical Conjecturing over Large Formal Corpora. | Thibault Gauthier, Cezary Kaliszyk, Josef Urban |
| 2016 | CIKM | A Standard for Aligning Mathematical Concepts. | Cezary Kaliszyk, Michael Kohlhase, Dennis Mller, Florian Rabe |
| 2016 | CPP | Towards a mizar environment for isabelle: foundations and language. | Cezary Kaliszyk, Karol Pak, Josef Urban |
| 2016 | FASE | Towards Formal Proof Metrics. | David Aspinall, Cezary Kaliszyk |
| 2016 | ITP | What's in a Theorem Name? | David Aspinall, Cezary Kaliszyk |
| 2015 | CADE | System Description: E.T. 0.1. | Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jir Vyskocil |
| 2015 | CPP | Premise Selection and External Provers for HOL4. | Thibault Gauthier, Cezary Kaliszyk |
| 2015 | CPP | Certified Connection Tableaux Proofs for HOL Light and TPTP. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | IJCAI | Efficient Semantic Features for Automated Reasoning over Large Theories. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | ITP | Learning to Parse on Aligned Corpora (Rough Diamond). | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | LPAR | Sharing HOL4 and HOL Light Proof Knowledge. | Thibault Gauthier, Cezary Kaliszyk |
| 2015 | LPAR | FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. | Cezary Kaliszyk, Josef Urban |
| 2015 | LPAR | Improving Statistical Linguistic Algorithms for Parsing Mathematics. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | TABLEAUX | Efficient Low-Level Connection Tableaux. | Cezary Kaliszyk |
| 2014 | CADE | Beagle as a HOL4 external ATP method. | Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish |
| 2014 | CADE | Machine Learner for Automated Reasoning 0.4 and 0.5. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2013 | CADE | Initial Experiments on Deriving a Complete HOL Simplification Set. | Cezary Kaliszyk, Thomas Sternagel |
| 2013 | CADE | PRocH: Proof Reconstruction for HOL Light. | Cezary Kaliszyk, Josef Urban |
| 2013 | CADE | Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. | Cezary Kaliszyk, Josef Urban |
| 2013 | ITP | Scalable LCF-Style Proof Translation. | Cezary Kaliszyk, Alexander Krauss |
| 2013 | ITP | MaSh: Machine Learning for Sledgehammer. | Daniel Khlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban |
| 2013 | ITP | Communicating Formal Proofs: The Case of Flyspeck. | Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers |
| 2013 | LPAR | Lemma Mining over HOL Light. | Cezary Kaliszyk, Josef Urban |
| 2012 | CADE | Initial Experiments with External Provers and Premise Selection on HOL Light Corpora. | Cezary Kaliszyk, Josef Urban |
| 2011 | CPP | Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem. | Cezary Kaliszyk, Henk Barendregt |
| 2011 | ESOP | General Bindings and Alpha-Equivalence in Nominal Isabelle. | Christian Urban, Cezary Kaliszyk |
| 2011 | SAC | Quotients revisited for Isabelle/HOL. | Cezary Kaliszyk, Christian Urban |
| 2008 | AISC | Automating Side Conditions in Formalized Partial Functions. | Cezary Kaliszyk |
| 2004 | ICWE | SIE - Intelligent Web Proxy Framework. | Grzegorz Andruszkiewicz, Krzysztof Ciebiera, Marcin Gozdalik, Cezary Kaliszyk, Mateusz Srebrny |