A New Machine-checked Proof of Strong Normalisation for Display Logic

1 Introduction Sequent calculi provide a rigorous basis for meta-theoretic studies of logics. The central theorem is cut-elimination which states that detours through lemmata can be avoided, and it can be used to show many important logical properties like consistency, interpolation, and Beth definability. Cut-free sequent calculi are also useful for automated deduction [14], nonclassical extensions of logic programming [22], and studying deep connections between cut elimination, lambda calculi and functional programming. Sequent calculi, and their extensions, therefore play an important role in theoretical computer science