Iris van der Giessen

Iris van der Giessen, Ian Shillito

Uniform interpolation is a strong form of interpolation providing an interpretation of propositional quantifiers within a propositional logic. Pitts' seminal work establishes this property for intuitionistic propositional logic relying on a sequent calculus in which naïve backward proof-search terminates. This constructive approach has been adapted to a wide range of logics, including intuitionistic modal logics. Surprisingly, no intuitionistic modal logic with independent box and diamond has yet been shown to satisfy uniform interpolation. We fill in this gap by proving the uniform interpolation property for Constructive K (CK) and Wijesekera's K (WK). We build on Pitts' technique by exploiting existing terminating calculi for CK and WK, which we prove to eliminate cut, and formalise all our results in the proof assistant Rocq. Together, our results constitute the first positive uniform interpolation results for intuitionistic modal logics with diamond.

Marta Bílková, Malvin Gattinger, Iris van der Giessen et al.

Advances in Modal Logic (AiML) was founded in 1995 as an initiative devoted to presenting an up-to-date picture of research in modal logic and its many applications. It combines a conference series with volumes arising from the conferences, and has become the flagship international forum for work on all aspects of modal logic. Over the past three decades, AiML has both recorded and helped shape developments across the field, bringing together semantic, proof-theoretic, algebraic, topological, computational, philosophical, and applied perspectives on modal and related logics. Exactly thirty years after the first AiML conference, AiML 2026, the sixteenth conference in the series, is organized by the Institute of Logic, Language and Computation (ILLC) of the University of Amsterdam. The conference takes place in Amsterdam, the Netherlands, from 29 June to 3 July 2026. This volume contains abstracts of invited talks and full papers accepted for the conference. Beginning with AiML 2026, the proceedings are published open access via Electronic Proceedings in Theoretical Computer Science (EPTCS).