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.
Original 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
Publication 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 Dive into the research topics of 'A games model of bunched implications'. Together they form a unique fingerprint.

Cite this