(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.