Type systems for concurrent programming calculi

Abstract

We explore the role of types in models of concurrent computation, particularly in the concrete setting of the asynchronous π-calculus. The major theme of this work may be summarized by the slogan-"Wherever you see structure, think of types". We propose type annotations not merely to channels, but also to the highly structured set of processes. The type system guarantees that well typed expressions cannot go wrong. Polymorphic process types formalize extant informal ideas regarding the channel passing and process passing approaches to process mobility. Further, subtyping relation between process types distinguishes between true concurrency and nondeterministic choice.