A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic

Abstract

We port Dawson and Goré’s general framework of deep embeddings of derivability from Isabelle to Coq. By using lists instead of multisets to encode sequents, we enable the encoding of genuinely substructural logics in which some combination of exchange, weakening and contraction are not admissible. We then show how to extend the framework to encode the linear nested sequent calculus LNSKt of Goré and Lellmann for the tense logic Kt and prove cut-elimination and all required proof-theoretic theorems in Coq, based on their pen-and-paper proofs. Finally, we extract the proof of the cut-elimination theorem to obtain a formally verified Haskell program that produces cut-free derivations from those with cut. We believe it is the first published formally verified computer program for eliminating cuts in any proof calculus. Show more