Publications

Two papers co-authored by our team member Ian Shillito have been published in the proceedings of the 13th International Joint Conference on Automated Reasoning (IJCAR 2026), held in Lisbon, Portugal, as part of FLoC 2026. Both papers extend Pitts’ proof-theoretic technique for uniform interpolation to new intuitionistic modal settings, and both come with full mechanisations in the Rocq proof assistant.

• Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM by Hugo Férée and Ian Shillito. Pitts’ technique had so far only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. This paper adapts it to the intuitionistic multi-succedent setting, focusing on the intuitionistic modal logic KM: a novel multi-succedent sequent calculus is designed that terminates and eliminates cut, yielding decidability, and is then used to construct uniform interpolants for KM. By (re)proving the algebraisability of KM, the coherence of the class of KM-algebras follows.

  [Read More]

Our paper “Polymorphism Meets DHOL” by Rhea Ranalter, Florian Rabe, and Cezary Kaliszyk has been officially published as part of LIPIcs, Volume 378, FSCD'26.

DHOL (Dependent Higher-Order Logic) is a powerful logic with dependent types and strong ATP support. This paper develops polymorphic DHOL (PDHOL), extending the expressivity of DHOL while retaining its simple definition and automation, with a sound and complete translation to polymorphic HOL implemented in a logic-embedding tool.

We are happy to announce a series of new papers from our team, all accepted for publication. The work spans two intertwined themes: large-scale LLM-assisted autoformalization of mathematical textbooks, and machine learning guidance for higher-order automated theorem proving. See our Publications page for details.

• Learning-Guided Higher-Order Automated Reasoning for Isabelle/HOL. We present higher-order extensions of ENIGMA and Deepire — the two prominent learning-guided reasoning systems for the E and Vampire provers — and evaluate them on a large Isabelle/HOL corpus emulating Sledgehammer, observing consistent improvement across the board.

  [Read More]