Milner's bigraphs [1] are a general framework for reasoning about distributed and concurrent programming languages. Notably, it has been designed to encompass both the -calcul...
We generalise Fiore et al's account of variable binding for untyped cartesian contexts and Tanaka's account of variable binding for untyped linear contexts to give an ac...