License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.325
URN: urn:nbn:de:0030-drops-54234
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5423/
Go to the corresponding LIPIcs Volume Portal

Brotherston, James ; Villard, Jules

Sub-classical Boolean Bunched Logics and the Meaning of Par

pdf-format:
20.pdf (0.5 MB)

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 Hilbert-style 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 heap-like memory models of separation logic, in which disjunction can be interpreted as a property of intersection operations over heaps.

BibTeX - Entry

@InProceedings{brotherston_et_al:LIPIcs:2015:5423,
  author =	{James Brotherston and Jules Villard},
  title =	{{Sub-classical Boolean Bunched Logics and the Meaning of Par}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{325--342},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5423},
  URN =		{urn:nbn:de:0030-drops-54234},
  doi =		{10.4230/LIPIcs.CSL.2015.325},
  annote =	{Keywords: Bunched logic, linear logic, modal logic, Kripke semantics, model theory}
}

Keywords: Bunched logic, linear logic, modal logic, Kripke semantics, model theory
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI