Research

Possible worlds and resources: The semantics of BI


Reference:

Pym, D. J., O'Hearn, P. W. and Yang, H., 2004. Possible worlds and resources: The semantics of BI. Theoretical Computer Science, 315 (1), pp. 257-305.

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Abstract

The logic of bunched implications, BI, is a substructural system which freely combines an additive (intuitionistic) and a multiplicative (linear) implication via bunches (contexts with two combining operations, one which admits Weakening and Contraction and one which does not). BI may be seen to arise from two main perspectives. On the one hand, from proof-theoretic or categorical concerns and, on the other, from a possible-worlds semantics based on preordered (commutative) monoids. This semantics may be motivated from a basic model of the notion of resource. We explain BI's proof-theoretic, categorical and semantic origins. We discuss in detail the question of completeness, explaining the essential distinction between BI with and without perpendicular to (the unit of boolean OR). We give an extensive discussion of BI as a semantically based logic of resources, giving concrete models based on Petri nets, ambients, computer memory, logic programming, and money. (C) 2003 Published by Elsevier B.V.

Details

Item Type Articles
CreatorsPym, D. J., O'Hearn, P. W. and Yang, H.
DOI10.1016/j.ics.2003.11.020
DepartmentsFaculty of Science > Computer Science
RefereedYes
StatusPublished
ID Code5452
Additional InformationID number: ISI:000221372000011

Export

Actions (login required)

View Item