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. After presenting the type
system and formal proofs of its correctness, we show encodings of the
lambda-calculus and typical concurrent objects in the deadlock-free
fragment of the calculus and demonstrate how type information can be
used for reasoning about program behavior.