Context-free session types (CFSTs) support expressive communication protocols, but programming with them tends to expose the linear threading of endpoints in both types and terms. This resource-passing style makes modular session programs cumbersome, especially when a component uses only a prefix of one or more protocols and returns the residual endpoints to its caller.
We extend CFSTs with borrowing. A borrow splits a session type into a borrowed protocol prefix and a residual suffix; for CFSTs, this split must be computed modulo the equational theory of sequential composition, choices, skipping behavior, and recursion. The resulting calculus supports direct-style use of session endpoints while preserving the linear invariant that communication advances protocol state.
A key novelty is the distinction between local and remote borrows. Local borrows remain in one process, where ordered linear typing guarantees that the borrowed prefix is processed before the residual suffix. Remote borrows may cross process boundaries; they require explicit synchronization to ensure that the borrowed prefix is processed before the residual suffix. The calculus has a direct operational semantics, an algorithmic type system based on constraints, and a translation to a lower-level calculus with explicit synchronization.