A games model of bunched implications


McCusker, G. and Pym, D., 2007. A games model of bunched implications. In: Duparc, J. and Henzinger, T. A., eds. Computer Science Logic: Proceedings of 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL.Vol. 4646. Berlin, Germany: Springer, pp. 573-588. (Lecture Notes in Computer Science)

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Official URL:


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.


Item Type Book Sections
CreatorsMcCusker, G.and Pym, D.
EditorsDuparc, J.and Henzinger, T. A.
DepartmentsFaculty of Science > Computer Science
ID Code18562
Additional Information21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings


Actions (login required)

View Item