Semantic cut elimination for the logic of bunched implications, formalized in Coq
summary
Semantic proof of cut elimination for BI is formalized in Coq and gives a concrete model: closed sets of cut-free principal bunches (closure under arbitrary intersections) that interpret connectives via closure and a monoidal product, yielding cut-free provability from model inclusion. Artifact: Coq formalization with 650 lines of specs and ≈2500 lines of proofs, using stdpp setoids and saturated rewriting. Proof is constructive so an extraction-ready algorithm exists but fails to run without further opacity and erasure work. Extensions for simple structural rules and an S4-like □ are handled with minor changes.
AI-written summary · about