Session Types Meet Polymorphism and Dependent Types

on YouTube ↗50m

" summary

Introduces session types for specifying bidirectional protocols in concurrent functional programming and shows how they guide server/client implementations. Covers two recent advances: FreeST2’s polymorphic context-free session types (improving modularity and removing a traditional restriction) and dependent session types (for more precise, flexible protocol descriptions), illustrated with examples and discussion of benefits and limitations.

AI-written summary · about

" chapters (15)

1. 0:00Start
2. 1:40Session Types in One Slide
3. 6:01Trajectory
4. 8:28The Arithmetic Service
5. 18:05Type syntax
6. 23:02Type formation-Session types
7. 25:13Session types are linear
8. 25:40A client
9. 29:25Defining subtyping
10. 31:17Subtyping by example
11. 33:37Subtyping rules
12. 38:00Extended example: generic binary arithmetic server
13. 39:24Revised grammar
14. 40:40Three examples
15. 42:30The grand unification

" related talks

• 54mShared Session Types for Safe, Practical ConcurrencyStephanie Balzer · Typelevel Summit Philadelphia 2019
• 28mDependent Session Protocols in Separation Logic from First PrinciplesRobbert Krebbers, Jonas Kastberg Hinrichsen, Jules Jacobs · ICFP 2023
• 23mPrecise Subtyping for Asynchronous Multiparty SessionsNobuko Yoshida, Alceste Scalas, Silvia Ghilezan, Ivan Prokić, Jovanka Pantović · POPL 2021
• 15mBorrowing From Session TypesHannes Saffrich, Janek Spaderna, Peter Thiemann · OOPSLA 2025
• 35mAsynchronous and Synchronous Mixed SessionsNobuko Yoshida, Kirstin Peters · ST30 2023
• 21mFair Termination of Binary SessionsLuca Padovani, Luca Ciccone · POPL 2022
• 23mProbabilistic Refinement Session TypesMarco Gaboardi, Qiancheng Fu, Ankush Das · PLDI 2026
• 25mA Logical Interpretation of Asynchronous Multiparty CompatibilityMarco Carbone, Sonia Marin, Carsten Schürmann · LOPSTR 2023