Type Systems for Bigraphs
- 199 Downloads
We propose a novel and uniform approach to type systems for (process) calculi, which roughly pushes the challenge of designing type systems and proving properties about them to the meta-model of bigraphs. Concretely, we propose to define type systems for the term language for bigraphs, which is based on a fixed set of elementary bigraphs and operators on these. An essential elementary bigraph is an ion, to which a control can be attached modelling its kind (its ordered number of channels and whether it is a guard), e.g. an input prefix of π-calculus. A model of a calculus is then a set of controls and a set of reaction rules, collectively a bigraphical reactive system (BRS). Possible advantages of developing bigraphical type systems include: a deeper understanding of a type system itself and its properties; transfer of the type systems to the concrete family of calculi that the BRS models; and the possibility of modularly adapting the type systems to extensions of the BRS (with new controls). As proof of concept we present a model of a π-calculus, develop an i/o-type system with subtyping on this model, prove crucial properties (including subject reduction) for this type system, and transfer these properties to the (typed) π-calculus.
KeywordsType System Main Lemma Typing Rule Type Soundness Type Judgment
Unable to display preview. Download preview PDF.
- 3.Bundgaard, M.N., Hildebrandt, T.T.: Bigraphical Semantics of Higher-Order Mobile Embedded Resources with Local Names. In: Proceedings of GT-VC 2005. ENTCS, vol. 154, pp. 7–29. Elsevier, Amsterdam (2006)Google Scholar
- 4.Bundgaard, M.N., Sassone, V.: Typed polyadic pi-calculus in bigraphs. In: Proceedings of PPDP 2006, pp. 1–12. ACM Press, New York (2006)Google Scholar
- 7.Jensen, O.H.: Mobile Processes in Bigraphs (Draft). PhD thesis, King’s College, University of Cambridge (submitted) (2007)Google Scholar
- 8.Jensen, O.H., Milner, R.: Bigraphs and Transitions. In: Proceedings of POPL 2003, pp. 38–49. ACM Press, New York (2003)Google Scholar
- 9.Jensen, O.H., Milner, R.: Bigraphs and mobile processes (revised). Technical Report UCAM-CL-TR-580, University of Cambridge (2004)Google Scholar
- 16.Milner, R.: Pure Bigraphs: Structure and dynamics. Inf. & Comp. 204(1) (2006)Google Scholar
- 17.Milner, R.: Local Bigraphs and Confluence: Two Conjectures. ENTCS 175(3) (June 2007)Google Scholar