UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Sub-classical Boolean Bunched Logics and the Meaning of Par

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 Green open access

[thumbnail of BBI_disjunction.pdf]
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.

Type: Proceedings paper
Title: Sub-classical Boolean Bunched Logics and the Meaning of Par
ISBN-13: 978-3-939897-90-3
Open access status: An open access version is available from UCL Discovery
DOI: 10.4230/LIPIcs.CSL.2015.325
Publisher version: http://www.dagstuhl.de/dagpub/978-3-939897-90-3
Language: English
Additional information: © James Brotherston and Jules Villard; licensed under Creative Commons License CC-BY. Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
Keywords: Bunched logic, linear logic, modal logic, Kripke semantics, model theory
UCL classification: UCL
UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/1474216
Downloads since deposit
15Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item