Parameterized Algebraic Protocols
summary
The work defines algebraic session types that name recursion like algebraic datatypes and claim type equivalence becomes linear-time nominal check instead of the doubly-exponential/context-free problem. An implementation (type checker + interpreter in HCo) is benchmarked against freST: generated types check under ~100 microseconds, while the context-free checker often times out or runs for hundreds of seconds. The system supports protocol parameterization and polymorphism, artifacts are available (PLDI paper and Zenodo) and the implementation is reusable.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:22Programming task with session types
- 2:32Context-free session types limits
- 3:34Type equivalence performance
- 4:37Algebraic session types intro
- 5:41Data types to protocol constructors
- 7:28Bidirectional protocol communication
- 9:10Parameterizing protocols over data
- 10:34Adding parameters to protocol types
- 12:03Modular services with parameters
- 13:46Implementation and benchmarking
- 14:52Paper contributions and type system
- 15:33Advantages of algebraic session types
- 16:16Q&A
related talks
22mProbabilistic Refinement Session Types
14mType-Sensitive Algebraic Macros
32mIntrinsically Typed Sessions with Callbacks
28mSemi-explicit polymorphic parameters
45mLogic Meta Programming for Functional Languages
21mPolymorphic Typestate for Session Types
19mMechanizing Session-Types using a Structural View: Enforcing Linearity without ...
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)