|
|
Technical Report HW-MACS-TR-0069
| Title | The Expressiveness of Generic Process Shape Types
|
|---|
| Authors | Jan Jakubuv, J.B. Wells |
|---|
| Date | 2009-07-30 |
|---|
| Abstract | The Expressiveness of Generic Process Shape Types
-------------------------------------------------
Meta* is a generic process calculus that can be instantiated by supplying
rewriting rules defining an operational semantics to make numerous process
calculi such as the π-calculus, the system of Mobile Ambients, and many of
their variants. Poly* is a generic type system that makes a sound type system
with principal types and a type inference algorithm for any instantiation of
Meta*. Poly* provides a generic notion of shape types which describe behavior
of processes by a direct description of allowed syntactic configurations.
This paper evaluates the expressiveness of generic process shape types by
comparing Poly* with three quite dissimilar type/static analysis systems in
the literature. The first comparison is with Turner's type system for the
π-calculus without type annotations (which is essentially Milner's system of
sorts). The second comparison is with an explicitly typed version of Mobile
Ambients by Cardelli and Gordon. Finally, the third comparison is with a
static analysis for BioAmbients developed by Nielson, Nielson, Priami, and
Rosa. We instantiate Meta* to the process calculi in question and compare
expressiveness of Poly* shape types with the predicates provided by the three
systems. We show that Poly* shape types can express much more precise
information than the previous type/static analysis systems and can also
express essentially the same information as the previous systems.
To do the comparisons, we needed to alter how Meta* handles α-conversion in
order to develop a new method for handling name restriction in Poly*. |
|---|
| Group | ULTRA |
|---|
| Notes | |
|---|
| Download |   |
|---|
|
|
