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 pi-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 pi-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) pi-calculus.
Type Systems for Bigraphs / E. Elsborg; T. T. Hildebrandt; D. Sangiorgi. - STAMPA. - 5474:(2009), pp. 126-140. (Intervento presentato al convegno Trustworthy Global Computing, 4th International Symposium tenutosi a Barcelona, Spain nel November 3-4, 2008).
Type Systems for Bigraphs
SANGIORGI, DAVIDE
2009
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 pi-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 pi-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) pi-calculus.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.