Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site Spatial and behavioral types in the pi-calculus
Lucia Acciai, Michele Boreale
abstract:
We present a framework that combines ideas from spatial logics and Igarashi and Kobayashi's behavioural type systems, drawing benefits from both. In our approach, type systems for the pi-calculus are introduced where newly declared (restricted) names are annotated with spatial process properties predicating on those names, that are expected to hold in the scope of the declaration. Types are akin to CCS terms and account for the abstract behaviour of the processes and their "shallow" spatial structure. The type systems relies on spatial model checking, but on types rather than on processes. Type soundness theorems are given ensuring that, for a certain class of spatial properties, well-typed programs are also well-annotated, in the sense that processes in the scope of any restriction do satisfy the corresponding annotation, at run-time. The considered class of properties is rather general and, differently from previously proposed systems, includes both safety and liveness ones and it is not limited to invariant formulae. We also elaborate a distinction between locally- and globally-checkable properties, corresponding to two distinct type systems with different degrees of compositionality and effectiveness.
