Advertisement

Type Systems for Bigraphs

  • Ebbe Elsborg
  • Thomas T. Hildebrandt
  • Davide Sangiorgi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5474)

Abstract

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.

Keywords

Type System Main Lemma Typing Rule Type Soundness Type Judgment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Birkedal, L., Debois, S., Elsborg, E., Hildebrandt, T.T., Niss, H.: Bigraphical models of context-aware systems. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 187–201. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Birkedal, L., Debois, S., Hildebrandt, T.T.: On the construction of sorted reactive systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 218–232. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  3. 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. 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
  5. 5.
    Damgaard, T.C., Birkedal, L.: Axiomatizing Binding Bigraphs. Nordic Journal of Computing 13(1-2), 58–77 (2006)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Igarashi, A., Kobayashi, N.: A generic type system for the Pi-calculus. TCS 311(1-3), 121–163 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Jensen, O.H.: Mobile Processes in Bigraphs (Draft). PhD thesis, King’s College, University of Cambridge (submitted) (2007)Google Scholar
  8. 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. 9.
    Jensen, O.H., Milner, R.: Bigraphs and mobile processes (revised). Technical Report UCAM-CL-TR-580, University of Cambridge (2004)Google Scholar
  10. 10.
    Kobayashi, N.: A type system for lock-free processes. Inf. & Comp. 177, 122–159 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    König, B.: A General Framework for Types in Graph Rewriting. Acta Inf. 42(4), 349–388 (2005); special issue: Types in concurrency, Part IIMathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Leifer, J.J., Milner, R.: Transition systems, link graphs, and Petri nets. MSCS 16(6), 989–1047 (2006)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Milner, R.: Bigraphs for petri nets. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 686–701. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. 15.
    Milner, R.: Axioms for bigraphical structure. MSCS 15(6), 1005–1032 (2005)MathSciNetzbMATHGoogle Scholar
  16. 16.
    Milner, R.: Pure Bigraphs: Structure and dynamics. Inf. & Comp. 204(1) (2006)Google Scholar
  17. 17.
    Milner, R.: Local Bigraphs and Confluence: Two Conjectures. ENTCS 175(3) (June 2007)Google Scholar
  18. 18.
    Pierce, B.C., Sangiorgi, D.: Typing and Subtyping for Mobile processes. MSCS 6(5), 409–453 (1996)MathSciNetzbMATHGoogle Scholar
  19. 19.
    Sangiorgi, D., Walker, D.: The Pi-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  20. 20.
    Weiser, M.: Hot Topics – Ubiquitous Computing. IEEE Computer 26(10), 71–72 (1993)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Ebbe Elsborg
    • 1
  • Thomas T. Hildebrandt
    • 1
  • Davide Sangiorgi
    • 2
  1. 1.IT University of Copenhagen (ITU)Denmark
  2. 2.Università di BolognaItaly

Personalised recommendations