The role of uniform interpolation in structural proof theory

In this talk I present a proof method to prove uniform interpolation in intermediate, modal and intuitionistic modal logics that applies to any such logic that has a sequent calculus with certain desirable properties. I illustrate the method by proving uniform interpolation for Lax Logic, an intuitionistic modal logic with applications in various areas, ranging from algebraic logic to hardware verification. I furthermore explain what general conclusion about the existence of sequent calculi for intermediate, modal and intuitionistic modal logics can be drawn from the method.