So what's the difference between a session type and an ordinary type anyway?
summary
Session types differ from ordinary types because they are substructural (linear), they distinguish global vs local specifications, and their channel behavior actually changes: channel types evolve during interaction, requiring a proof of preservation/progress that uses multiset-rewriting semantics and the fact that type changes are internal (private) actions. Asynchrony forces use of a continuation channel in each message, enabling a compilation of functional expressions to processes that pass destinations (so applications carry an extra continuation), which yields a typed model of futures; an implementation used in coursework lets students run and typecheck these programs.
AI-written summary · about
chapters (13)
- 0:00Session types introduction
- 1:46Similarities with ordinary types
- 2:07Global vs local types
- 3:10Substructural type evolution
- 4:10Session versus functional types
- 6:37Type evolution example
- 8:41Asynchronous communication
- 11:09Beyond binary communication
- 14:41Linear and nonlinear types
- 17:56Compiling to ordinary types
- 22:29What's special about session types
- 24:56Global session type questions
- 27:47Q&A
related talks
32mIntrinsically Typed Sessions with Callbacks
21mPolymorphic Typestate for Session Types
20mMessage-Observing Sessions
40mTypes and Erlang from Dialyzer to (...)
19mMechanizing Session-Types using a Structural View: Enforcing Linearity without ...
24mTowards Quantum Multiparty Session Types
26mFusing Session-Typed Concurrent Programming into Functional Programming
16mIntriniscly-Typed Interpretation of Linear Languages