Borrowing From Session Types
summary
Proposes BGV, a session‑type API that replaces resource‑passing with borrowing via a split primitive that carves a channel into a single‑action borrow and a remainder, and models borrows as a pair of oneshot cells so the borrower waits for and then hands off the underlying channel. Gives a type system based on ordered linear typing, proves type preservation and deadlock freedom by a translation to PGV with priorities, delivers a mechanized, verified translation and a decidable, algorithmic external language plus reusable artifacts.
AI-written summary · about
chapters (8)
- 0:00Session types intro
- 0:13Resource passing style
- 3:06Multiple continuations issues
- 4:52Borrowing style API
- 7:00Ordering and BI context
- 9:08Borrowing across threads
- 12:45Type system details
- 14:11Q&A
related talks
54mShared Session Types for Safe, Practical Concurrency
14mMultiparty GV: Functional Multiparty Session Types with Certified Deadlock Fre...
50mSession Types Meet Polymorphism and Dependent Types
23mPrecise Subtyping for Asynchronous Multiparty Sessions
28mDependent Session Protocols in Separation Logic from First Principles
46mExploring lending async iterators
35mAsynchronous and Synchronous Mixed Sessions
16mVerified Lock-Free Session Channels with Linking