Prior work has established the logical connection between linear sequent calculus and session-typed message-passing concurrent computation. The basic system was shown to guarantee strong properties such as session fidelity and deadlock freedom. In this thesis, I extend the basic type system with intersection and union types in order to express multiple behavioral properties of processes in a single type. In the presence of equirecursive types and a natural notion of subtyping, the resulting system turns out to be strong enough to statically prove many useful properties. I present the system and illustrate its expressive power with examples.