ABSTRACT. We propose a new type system for deadlock-free session-typed π-calculus, a core concurrent programming language, by integrating for the first time, two separate lines of work. The first is the propositions-as-types approach by Caires and Pfenning, which provides a linear logic foundation for session types and guarantees deadlock-freedom. The second is Kobayashi’s approach in which types are annotated with priorities for detecting cyclic dependencies between communication operations. The outcome is a new and more expressive variant of classical linear logic with a proof assignment that gives a session type system with Kobayashi-style priorities.