Syntactic theory for bigraphs

I investigate and develop theory for term languages for a variant of bigraphs with binding, thus building the formal foundation for a (term-based) tool for bigraphical reactive systems. I present two main results (developed with co-authors). First, I give an axiomatization of structural congruence (graph equivalence) for binding bigraphs. Along the way, I devise a term language for binding bigraphs and prove a series of normal form theorems for binding bigraphs. Second, using these results, I give a complete inductive characterization of matching in bigraphs — essentially, for describing when and where a bigraphical reaction rule can be applied. I include an introduction to the goals of my Ph.D. project and explain how it relates to the goals of the BPL project. Moreover, I outline a number of future challenges and include a litterature study for future work