Brotherston, J; Villard, J; (2015) Sub-classical Boolean Bunched Logics and the Meaning of Par. In: Kreutzer, S, (ed.) (pp. pp. 325-342). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Preview

Text BBI_disjunction.pdf - Published Version Download (626kB) | Preview

Abstract

We investigate intermediate logics between the bunched logics Boolean BI and Classical BI, obtained by combining classical propositional logic with various flavours of Hyland and De Paiva’s full intuitionistic linear logic. Thus, in addition to the usual multiplicative conjunction (with its adjoint implication and unit), our logics also feature a multiplicative disjunction (with its adjoint co-implication and unit). The multiplicatives behave “sub-classically”, in that disjunction and conjunction are related by a weak distribution principle, rather than by De Morgan equivalence. We formulate a Kripke semantics, covering all our sub-classical bunched logics, in which the multiplicatives are naturally read in terms of resource operations. Our main theoretical result is that validity according to this semantics coincides with provability in a corresponding Hilbertstyle proof system. Our logical investigation sheds considerable new light on how one can understand the multiplicative disjunction, better known as linear logic’s “par”, in terms of resource operations. In particular, and in contrast to the earlier Classical BI, the models of our logics include the heaplike memory models of separation logic, in which disjunction can be interpreted as a property of intersection operations over heaps.

Download activity - last month

Export as XMLCSVJSON

Download activity - last 12 months

Export as JSONCSVXML

Downloads by country - last 12 months

Export as XMLCSVJSON

Archive Staff Only

View Item