Typing and subtyping for mobile processes. (English) Zbl 0861.68030

Pierce, Benjamin; Sangiorgi, Davide

Math. Struct. Comput. Sci. 6, No. 5, 409-453 (1996).

Summary: The \(\pi\)-calculus is a process algebra that supports mobility by focusing on the communication of channels. Milner’s presentation of the \(\pi\)-calculus includes a type system assigning arities to channels and enforcing a corresponding discipline in their use. We extend Milner’s language of types by distinguishing between the ability to read from a channel, the ability to write to a channel, and the ability both to read and to write. This refinement gives rise to a natural subtype relation similar to those studied in typed \(\lambda\)-calculi. The greater precision of our type discipline yields stronger versions of standard theorems on the \(\pi\)-calculus. These can be used, for example, to obtain the validity of \(\beta\)-reduction for the more efficient of Milner’s encodings of the call-by-value \(\lambda\)-calculus, which fails in the ordinary \(\pi\)-calculus. We define the syntax, typing, subtyping, and operational semantics of our calculus, prove that the typing rules are sound, apply the system to Milner’s \(\lambda\)-calculus encodings, and sketch extensions to higher-order process calculi and polymorphic typing.

MSC:

68Q10	Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
03B40	Combinatory logic and lambda calculus
68Q55	Semantics in the theory of computing

Keywords:

\(\pi\)-calculus; Milner’s language