Linearity and the pi-calculus

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 recove r important static information about a process's behavior. In particular, w e can guarantee that two processes communicating over a linear channel cann ot interfere with other communicating processes. 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 h ow reductions on linear channels induce a useful "partial confluence" of pr ocess behaviors. For an extended example of the theory, we prove the validi ty of a tail-call optimisation for higher-order functions represented as pr ocesses.