A Games Model of Bunched Implications
McCusker, Guy; Pym, David
HPL-2007-100
External - Copyright Consideration
Keyword(s): bunched logic; games semantics; alpha- lambda-calculus
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. Publication Info: Lecture Notes in Computer Science, Proceedings CSL 2007.
15 Pages
Back to Index
| 
Printable version
