Expressiveness of Generic Process Shape Types

TL;DR

This paper extends the Poly* shape type system to include name restriction, demonstrating increased expressiveness over other process calculi and highlighting benefits like polymorphism and type inference.

Contribution

The main contribution is the extension of the Poly* shape type system to support name restriction, enhancing its expressiveness and practical applicability.

Findings

Shape types are more expressive than implicitly typed pi-calculus.

Shape types outperform explicitly typed Mobile Ambients.

Extension facilitates polymorphism and type inference.

Abstract

Shape types are a general concept of process types which work for many process calculi. We extend the previously published Poly* system of shape types to support name restriction. We evaluate the expressiveness of the extended system by showing that shape types are more expressive than an implicitly typed pi-calculus and an explicitly typed Mobile Ambients. We demonstrate that the extended system makes it easier to enjoy advantages of shape types which include polymorphism, principal typings, and a type inference implementation.