An algebraic glimpse at bunched implications and separation logic

DOI10.1007/978-3-030-76920-8_5arXiv1709.07063OpenAlexW2759139027MaRDI QIDQ6201543FDOQ6201543

Publication date: 25 March 2024

Published in: Outstanding Contributions to Logic (Search for Journal in Brave)

Abstract: We overview the logic of Bunched Implications (BI) and Separation Logic (SL) from a perspective inspired by Hiroakira Ono's algebraic approach to substructural logics. We propose generalized BI algebras (GBI-algebras) as a common framework for algebras arising via "declarative resource reading", intuitionistic generalizations of relation algebras and arrow logics and the distributive Lambek calculus with intuitionistic implication. Apart from existing models of BI (in particular, heap models and effect algebras), we also cover models arising from weakening relations, formal languages or more fine-grained treatment of labelled trees and semistructured data. After briefly discussing the lattice of subvarieties of GBI, we present a suitable duality for GBI along the lines of Esakia and Priestley and an algebraic proof of cut elimination in the setting of residuated frames of Galatos and Jipsen. We also show how the algebraic approach allows generic results on decidability, both positive and negative ones. In the final part of the paper, we gently introduce the substructural audience to some theory behind state-of-art tools, culminating with an algebraic and proof-theoretic presentation of (bi-)abduction.

Full work available at URL: https://arxiv.org/abs/1709.07063

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) General logic (03Bxx)

Cites Work

This page was built for publication: An algebraic glimpse at bunched implications and separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6201543)