A partially deadlock-free typed process calculus

Abstract

We propose a novel static type system for a process calculus, which ensures both partial deadlock-freedom and partial confluence. The key novel ideas are (1) introduction of the order of channel use as type information, and (2) classification of communication channels into reliable and unreliable channels based on their usage and a guarantee of the usage by the type system. We can ensure that communication on reliable channels never causes deadlock and also that certain reliable channels never introduce nondeterminism. With the type system, for example, the simply typed lambda-calculus can be encoded into the deadlock-free and confluent fragment of our process calculus; we can therefore recover behavior of the typed lambda-calculus in the level of process calculi. We also show that typical concurrent objects can also be encoded into the deadlock-free fragment.