Session types provide a formal framework to enforce rich communication protocols, ensuring correctness properties such as type safety and deadlock freedom. However, the traditional API of functional session type systems with first-class channels often leads to problems with modularity and composability. This paper proposes a new, alternative session type API based on borrowing, embodied in the core calculus BGV. The borrowing-based API enables building modular and composable code for session type clients without imposing clutter or undue limitations. Its basis is a novel type system, founded on ordered linear typing, for functional session types with an explicit operation for splitting ownership of channels. We establish the semantics of BGV via a type-preserving translation to PGV, a deadlock-free functional session type calculus. We establish type safety and deadlock freedom for BGV by this translation. We also present an external version of BGV that supports use of borrow notation. We developed an algorithmic version of the type system that includes a mechanized verified translation from the external language to BGV. This part establishes decidable type checking.

We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs in linear time. Algebraic protocols in combination with polymorphism increase expressiveness and modularity by facilitating new ways of parameterizing and composing session types.