Publications

📚 Conference Papers

1. Rhea Ranalter, Florian Rabe, Cezary Kaliszyk:
   ✦ Polymorphism Meets DHOL.
   In LIPIcs, Volume 378, FSCD 2026.
   [ pdf | doi | proceedings | bibtex ]

2. Hugo Férée, Ian Shillito:
   ✦ Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM.
   In LNCS, Volume 16688, IJCAR 2026.
   [ pdf | doi | proceedings | bibtex ]

3. Iris van der Giessen, Ian Shillito:
   ✦ Uniform Interpolation with Constructive Diamond.
   In LNCS, Volume 16688, IJCAR 2026.
   [ pdf | doi | proceedings | bibtex ]

📄 Preprints

Preprints of papers accepted for publication, currently in press.

1. Chad E. Brown, Cezary Kaliszyk, Josef Urban:
   ✦ Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents.
   [ arXiv | dblp | bibtex ]

2. Dustin Bryant, Jonathan Julián Huerta y Munive, Cezary Kaliszyk, Josef Urban:
   ✦ Munkres’ General Topology Autoformalized in Isabelle/HOL.
   [ arXiv | dblp | bibtex ]

3. Jeremy Lindsay, Cezary Kaliszyk, Christine Rizkallah:
   ✦ Optimising Metamath Proofs for Human Working Memory.
   [ pdf ] (Accepted to CICM'26)

4. Jan Jakubův, Cezary Kaliszyk, Martin Suda.
   ✦ Learning-Guided Higher-Order Automated Reasoning for Isabelle/HOL.
   [ pdf ] (Accepted to CICM'26)