Intrinsically Typed Sessions with Callbacks
summary
Claims a practical embedding of session types that avoids host-language linear types by representing protocols as an indexed command data structure of callbacks and interpreting it in Agda, with the interpreter as the single trusted locus for linearity. Encodings handle branching, recursion (with an unroll client command and resumptions), multichannel and higher-order sessions; multichannel extension claims deadlock freedom by construction. Development includes Agda-checked code and reusable artifacts, but the interpreter carries a manual proof obligation and some termination pragmas.
AI-written summary · about
chapters (15)
- 0:00Introduction to session types
- 0:22Intrinsically typed sessions with callbacks
- 3:50Safe session types without linear types
- 4:31Callbacks for session types
- 6:58Improving callback APIs in functional languages
- 8:00Command structure for session protocols
- 10:06Session types in Agda
- 13:01Interpreter correctness proofs
- 13:22Selection and choice in protocols
- 15:34Modular protocol implementations
- 17:18Recursion in session types
- 20:49Context-free and multi-channel sessions
- 22:13State monads and callbacks
- 23:16Summary and future work
- 24:22Q&A
related talks
16mIntriniscly-Typed Interpretation of Linear Languages
31mSo what's the difference between a session type and an ordinary type anyway?
19mMechanizing Session-Types using a Structural View: Enforcing Linearity without ...
54mShared Session Types for Safe, Practical Concurrency
28mA Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in
21mPolymorphic Typestate for Session Types
20mParameterized Algebraic Protocols
20mMessage-Observing Sessions