Analysing Input/Output-Capabilities of Mobile Processes with a Generic Type System

We introduce a generic type system (based on Milner's sort system) for the synchronous polyadic -calculus, allowing us to mechanise the analysis of input/output capabilities of mobile processes. The parameter of the generic type system is a lattice-ordered monoid, the elements of which are used to describe the capabilities of channels with respect to their input/output-capabilities. The type system can be instantiated in order to check process properties such as upper and lower bounds on the number of active channels, confluence and absence of blocked processes.

• Type: Conference
• Year: 2000
• Where: ICALP
• Authors: Barbara König
• Keywords: Generic Type, ICALP 2000, Milner's Sort System, Programming Languages, Type System