@inproceedings{5c35dc84d27a47f19fbff74ad5e0c3da,
title = "A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic",
abstract = "We port Dawson and Gor{\'e}{\textquoteright}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{\'e} 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.",
keywords = "Coq, Cut-elimination, Extraction, Formalised proof theory, Linear nested sequent calculus, Program synthesis, Tense logic",
author = "Caitlin D{\textquoteright}Abrera and Jeremy Dawson and Rajeev Gor{\'e}",
note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2021, co-located with the 13th International Symposium on Frontiers of Combining Systems, FroCoS 2021 ; Conference date: 06-09-2021 Through 09-09-2021",
year = "2021",
doi = "10.1007/978-3-030-86059-2_17",
language = "English",
isbn = "9783030860585",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "281--298",
editor = "Anupam Das and Sara Negri",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Proceedings",
address = "Germany",
}