Modal μ-types for processes

Introduces a new paradigm for concurrency, called behaviours-as-types. In this paradigm, types are used to convey information about the behaviour of processes: while terms correspond to processes, types correspond to behaviours. We apply this paradigm to Winskel's (1994) process algebra. Its types are similar to Kozen's (1983) modal /spl mu/-calculus; hence, they are called modal /spl mu/-types. We prove that two terms having the same type denote two processes which behave in the some way, that is, they are bisimilar. We give a sound and complete compositional typing system for this language. Such a system naturally also recovers the notion of bisimulation on open terms, allowing us to deal with processes with undefined parts in a compositional manner.