Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq

TL;DR

This paper formalizes a semantic proof of cut elimination for the logic of bunched implications (BI) within Coq, providing a more modular and scalable approach than traditional methods, with implications for separation logic.

Contribution

It introduces a semantic, Coq-based proof of cut elimination for BI, extending its applicability to enriched variants with structural rules and modalities.

Findings

Semantic proof is more modular and elegant.

Proof scales to extensions with structural rules and modalities.

Avoids complex cut reductions and inversions.

Abstract

The logic of bunched implications (BI) is a substructural logic that forms the backbone of separation logic, the much studied logic for reasoning about heap-manipulating programs. Although the proof theory and metatheory of BI are mathematically involved, the formalization of important metatheoretical results is still incipient. In this paper we present a self-contained formalized, in the Coq proof assistant, proof of a central metatheoretical property of BI: cut elimination for its sequent calculus. The presented proof is *semantic*, in the sense that is obtained by interpreting sequents in a particular "universal" model. This results in a more modular and elegant proof than a standard Gentzen-style cut elimination argument, which can be subtle and error-prone in manual proofs for BI. In particular, our semantic approach avoids unnecessary inversions on proof derivations, or the uses of cut reductions and the multi-cut rule. Besides modular, our approach is also robust: we demonstrate how our method scales, with minor modifications, to (i) an extension of BI with an arbitrary set of \emph{simple structural rules}, and (ii) an extension with an S4-like $\Box$ modality.