# A linear type system for pi calculus

## Marco Giunti, INRIA and LIX, Ecole Polytechnique, France

(Joint work with Vasco Vasconcelos)

We present a type-checking algorithm for establishing a session-based
discipline in the pi calculus of Milner, Parrow and Walker. Our
session types are qualified as linear or unrestricted. Linearly typed
communication channels are guaranteed to occur in exactly one thread,
possibly multiple times; afterwards they evolve as unrestricted
channels. Session protocols are described by a type constructor that
denotes the two ends of a same communication channel. We ensure the
soundness of the algorithm by showing that processes consuming all
linear resources are accepted by a typing system which preserves types
during the computation.