Semantic cut elimination for the logic of bunched implications, formalized in Coq
Distinguished Paper AwardRemote
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 simple structural rules, and (ii) an extension with an S4-like $\Box$ modality.
Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 15:10
|Semantic cut elimination for the logic of bunched implications, formalized in CoqDistinguished Paper AwardRemote|
Dan Frumin University of GroningenPre-print Media Attached
|Undecidability, Incompleteness, and Completeness of Second-Order Logic in CoqRemote|
|Formalising Lie algebrasRemote|
Oliver Nash Imperial College, LondonPre-print Media Attached
|A Machine-Checked Direct Proof of the Steiner-Lehmus TheoremInPerson|
Ariel Kellison Cornell UniversityPre-print