### Abstract

Language | English |
---|---|

Title of host publication | Computer Science Logic: Proceedings of 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings |

Editors | J Duparc, T A Henzinger |

Place of Publication | Berlin, Germany |

Publisher | Springer |

Pages | 573-588 |

Number of pages | 16 |

Volume | 4646 |

ISBN (Electronic) | 978-3-540-74915-8 |

ISBN (Print) | 978-3-540-74914-1 |

DOIs | |

Status | Published - 2007 |

Event | 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL - Switzerland, Lausanne, Switzerland Duration: 11 Sep 2007 → 15 Sep 2007 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

### Conference

Conference | 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL |
---|---|

Country | Switzerland |

City | Lausanne |

Period | 11/09/07 → 15/09/07 |

### Fingerprint

### Cite this

*Computer Science Logic: Proceedings of 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings*(Vol. 4646, pp. 573-588). (Lecture Notes in Computer Science). Berlin, Germany: Springer. DOI: 10.1007/978-3-540-74915-8_42

**A games model of bunched implications.** / McCusker, Guy; Pym, David.

Research output: Chapter in Book/Report/Conference proceeding › Chapter

*Computer Science Logic: Proceedings of 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings.*vol. 4646, Lecture Notes in Computer Science, Springer, Berlin, Germany, pp. 573-588, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, 11/09/07. DOI: 10.1007/978-3-540-74915-8_42

}

TY - CHAP

T1 - A games model of bunched implications

AU - McCusker,Guy

AU - Pym,David

PY - 2007

Y1 - 2007

N2 - A game semantics of the ( − − *, →)-fragment of the logic of bunched implications, BI, is presented. To date, categorical models of BI have been restricted to two kinds: functor category models; and the category Cat itself. The game model is not of this kind. Rather, it is based on Hyland-Ong-Nickau-style games and embodies a careful analysis of the notions of resource sharing and separation inherent in BI. The key to distinguishing between the additive and multiplicative connectives of BI is a semantic notion of separation. The main result of the paper is that the model is fully complete: every finite, total strategy in the model is the denotation of a term of the αλ-calculus, the term language for the fragment of BI under consideration.

AB - A game semantics of the ( − − *, →)-fragment of the logic of bunched implications, BI, is presented. To date, categorical models of BI have been restricted to two kinds: functor category models; and the category Cat itself. The game model is not of this kind. Rather, it is based on Hyland-Ong-Nickau-style games and embodies a careful analysis of the notions of resource sharing and separation inherent in BI. The key to distinguishing between the additive and multiplicative connectives of BI is a semantic notion of separation. The main result of the paper is that the model is fully complete: every finite, total strategy in the model is the denotation of a term of the αλ-calculus, the term language for the fragment of BI under consideration.

UR - http://dx.doi.org/10.1007/978-3-540-74915-8_42

U2 - 10.1007/978-3-540-74915-8_42

DO - 10.1007/978-3-540-74915-8_42

M3 - Chapter

SN - 978-3-540-74914-1

VL - 4646

T3 - Lecture Notes in Computer Science

SP - 573

EP - 588

BT - Computer Science Logic: Proceedings of 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings

PB - Springer

CY - Berlin, Germany

ER -