A games model of bunched implications

Guy McCusker; David Pym

doi:10.1007/978-3-540-74915-8_42

A games model of bunched implications

Research output: Chapter or section in a book/report/conference proceeding › Book chapter

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.

Original 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	https://doi.org/10.1007/978-3-540-74915-8_42
Publication status	Published - 2007
Event	21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL - Switzerland, Lausanne, Switzerland Duration: 11 Sept 2007 → 15 Sept 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/Territory	Switzerland
City	Lausanne
Period	11/09/07 → 15/09/07

Access to Document

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

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). Springer. https://doi.org/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 or section in a book/report/conference proceeding › Book chapter

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. https://doi.org/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). 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",

note = "21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL ; Conference date: 11-09-2007 Through 15-09-2007",

}

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

UR - https://www.scopus.com/pages/publications/38049048644

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

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

M3 - Book 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

A2 - Duparc, J

A2 - Henzinger, T A

PB - Springer

CY - Berlin, Germany

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

Y2 - 11 September 2007 through 15 September 2007

ER -

A games model of bunched implications

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this