Higher-order Contexts via Games and the Int-construction

TR-2009-117, Authors: Lars Birkedal, Mikkel Bundgaard, Søren Debois, Davide Grohmann and Thomas Hildebrandt

Lars Birkedal
Mikkel Bundgaard
Søren Debois
Davide Grohmann
Thomas Hildebrandt

January 2009

Abstract

Monoidal categories of acyclic graphs capture the notion of multi-hole context, pervasive in syntax and semantics. Milner's bigraphs is a recent example. We give a method for generalising such categories to monoidal closed categories of acyclic graphs. The method combines the Int-construction, lifting traced monoidal categories to compact closed ones; the recent formulation of sortings for reactive systems; and games for multiplicative linear logic. The closed categories obtained by our construction captures a notion of higher-order contexts. These encompass extensions to the traditional notion of context found in recent work on Milner's reactive systems and bigraphs. We demonstrate how technical devices employed in these extensions are in fact intrinsic to higher-order contexts. Finally, we use the method to construct higher-order bigraphs, recovering directed bigraphs as a limited instance.

---

Technical report TR-2009-117 in IT University Technical Report Series, January 2009.

Available as PDF.