The paper “Borrowing from Session Types”, co-authored by Hannes Saffrich, Janek Spaderna, Peter Thiemann, and Vasco T. Vasconcelos, was published in top 10% journal Proceedings of the ACM on Programming Languages (PACMPL) and was presented at OOPSLA 2025, that took place from October 12 to 18, 2025, in Singapore. This research was led by researchers at LASIGE and at the University of Freiburg, Germany.

Session types describe communication protocols. When incorporated in concurrent programming languages, session types ensure correctness properties such as type safety and absence of deadlocks.

Programming languages with session types exert a tight control on the state of communication channels, turning at times programming into a cumbersome task. Inspired by the Rust programming language, we introduce the idea of borrowing channels, allowing functions to consume part of channel protocols without being required to explicitly return the unused part of the channel.

The paper describes the language, its operational semantics and type system. It further develops an algorithmic version of the type system, which has been implemented. Part of the proofs is mechanised in the Agda programming language.

The paple is available here.