UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Possible worlds and resources: The semantics of BI

Pym, DJ; O'Hearn, PW; Yang, H; (2004) Possible worlds and resources: The semantics of BI. Theoretical Computer Science , 315 (1) pp. 257-305. 10.1016/j.tcs.2003.11.020.

Full text not available from this repository.


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 ⊥ (the unit of ∨). 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. © 2003 Published by Elsevier B.V.

Type: Article
Title: Possible worlds and resources: The semantics of BI
DOI: 10.1016/j.tcs.2003.11.020
UCL classification: UCL > School of BEAMS
UCL > School of BEAMS > Faculty of Engineering Science
URI: http://discovery.ucl.ac.uk/id/eprint/1342384
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item