Abstract
The economy and flexibility of the pi-calculus make it an attractive
object of theoretical study and a clean basis for concurrent
language design and implementation. However, such generality has a
cost: encoding higher-level features like functional computation in
pi-calculus throws away potentially useful information. We show how a
linear type system can be used to recover important static information
about a process's behaviour. In particular, we can guarantee that two
processes communicating over a linear channel cannot interfere with
other communicating processes. This enables more aggressive
optimisation of communications over linear channels and allows useful
refinements to the usual notions of process equivalence for
pi-calculus.
After developing standard results such
as soundness of typing, we focus on equivalences, adapting the
standard notion of barbed bisimulation to the linear setting and
showing how reductions on linear channels induce a useful ``partial
confluence'' of process behaviors.