Formalizing Cut Elimination of Coalgebraic Logics in Coq

In their work on coalgebraic logics, Pattinson and Schroder prove soundness, completeness and cut elimination in a generic sequent calculus for propositional multi-modal logics [1]. The present paper reports on a formalization of Pattinson's and Schroder's work in the proof assistant Coq that provides machine-checked proofs for soundness, completeness and cut elimination of their calculus. The formalization exploits dependent types to obtain a very concise deep embedding for formulas and proofs. The work presented here can be used to verify cut elimination theorems for different modal logics with considerably less effort in the future.