A games model of bunched implications

Guy McCusker, David Pym

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

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.
LanguageEnglish
Title of host publicationComputer Science Logic: Proceedings of 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings
EditorsJ Duparc, T A Henzinger
Place of PublicationBerlin, Germany
PublisherSpringer
Pages573-588
Number of pages16
Volume4646
ISBN (Electronic)978-3-540-74915-8
ISBN (Print)978-3-540-74914-1
DOIs
StatusPublished - 2007
Event21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL - Switzerland, Lausanne, Switzerland
Duration: 11 Sep 200715 Sep 2007

Publication series

NameLecture Notes in Computer Science
PublisherSpringer

Conference

Conference21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL
CountrySwitzerland
CityLausanne
Period11/09/0715/09/07

Fingerprint

Game
Fragment
Game Semantics
Model Category
Resource Sharing
Term
Categorical
Model
Functor
Multiplicative
Calculus
Logic
Style
Strategy
Semantics
Language

Cite this

McCusker, G., & Pym, D. (2007). A games model of bunched implications. In J. Duparc, & T. A. Henzinger (Eds.), 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.

Computer Science Logic: Proceedings of 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings. ed. / J Duparc; T A Henzinger. Vol. 4646 Berlin, Germany : Springer, 2007. p. 573-588 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingChapter

McCusker, G & Pym, D 2007, A games model of bunched implications. in J Duparc & TA Henzinger (eds), 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
McCusker G, Pym D. A games model of bunched implications. In Duparc J, Henzinger TA, editors, 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. Berlin, Germany: Springer. 2007. p. 573-588. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-540-74915-8_42
McCusker, Guy ; Pym, David. / A games model of bunched implications. Computer Science Logic: Proceedings of 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings. editor / J Duparc ; T A Henzinger. Vol. 4646 Berlin, Germany : Springer, 2007. pp. 573-588 (Lecture Notes in Computer Science).
@inbook{628ed5ebd4984395a8b8f31ec2413051,
title = "A games model of bunched implications",
abstract = "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.",
author = "Guy McCusker and David Pym",
year = "2007",
doi = "10.1007/978-3-540-74915-8_42",
language = "English",
isbn = "978-3-540-74914-1",
volume = "4646",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "573--588",
editor = "J Duparc and Henzinger, {T A}",
booktitle = "Computer Science Logic: Proceedings of 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings",

}

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 -