Generic process shape types and the Poly* system

Abstract

Shape types are a general concept of process types which allows verification of various properties of processes from various calculi. The key property is that shape types “look like processes”, that is, they resemble process structure and content. PolyV, originally designed by Makholm and Wells, is a type system scheme which can be instantiated to a shape type system for many calculi. Every PolyV instantiation has desirable properties including subject reduction, polymorphism, the existence of principal typings, and a type inference algorithm. In the first part of this thesis, we fix and describe inconsistencies found in the original PolyV system, we extend the system to support name restriction, and we provide a detailed proof of the correctness of the system. In the second part, we present a description of the type inference algorithm which we use to constructively prove the existence of principal typings. In the third part, we present various applications of shape types which demonstrate their advantages. Furthermore we prove that shape types can provide the same expressive power as and also strictly superior expressive power than predicates of three quite dissimilar analysis systems from the literature, namely, (1) an implicitly typed π-calculus, (2) an explicitly typed Mobile Ambients, (3) and a flow analysis system for BioAmbients.