A games model of bunched implications

Guy McCusker: A game semantics of the implication-only fragment of O'Hearn and Pym's Logic of Bunched Implications (BI) is presented. The model is based on Hyland-Ong-style innocent strategies, augmented with new conditions to capture the resource control aspects of the logic. It is shown that the model has the property of full completeness; that is, every finite element of the model is the denotation of a proof of BI. This is joint work with David Pym (HP Labs, Bristol).