Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM

Hugo Férée and Ian Shillito

Abstract

We adapt Pitts’ technique to intuitionistic multi-succedent calculi and construct uniform interpolants for KM. The results, including termination and cut-elimination, are mechanised in Rocq.

Paper Preprint Code

← All publications