1 Search Results for "Brotherston, James"

Document

DOI: 10.4230/LIPIcs.CSL.2015.325

Sub-classical Boolean Bunched Logics and the Meaning of Par

Authors: James Brotherston and Jules Villard

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

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.

Cite as

James Brotherston and Jules Villard. Sub-classical Boolean Bunched Logics and the Meaning of Par. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 325-342, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{brotherston_et_al:LIPIcs.CSL.2015.325,
  author =	{Brotherston, James and Villard, Jules},
  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 =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.325},
  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}
}

Refine by Author
1 Brotherston, James
1 Villard, Jules

Refine by Classification

Refine by Keyword
1 Bunched logic
1 Kripke semantics
1 linear logic
1 modal logic
1 model theory

Refine by Type
1 document

Refine by Publication Year
1 2015

1 Search Results for "Brotherston, James"

Sub-classical Boolean Bunched Logics and the Meaning of Par

Abstract

Cite as

Thanks for your feedback!

Could not send message