Multiparty Reactive Sessions
summary
Proposes MRS calculus combining multiparty session types with Synchronous Reactive Programming, adds broadcast, explicit pause/pose for logical instants, and event emissions; implements a shared message store, suspension operator and a tick reduction that clears memory each instant. Main deliverable is a session type system that enforces protocol conformance and proves input timeliness (every input is matched now or next instant) and bounded reactivity (no infinite computation inside an instant). Example: an auction encoding where bids aggregate per instant; metatheory proofs are provided.
AI-written summary · about
chapters (12)
- 0:00Multiparty reactive sessions intro
- 1:20Reactive programming basics
- 2:45Reactivity meets session types
- 5:38Auction protocol demo
- 8:05Auction system implementation
- 10:17Reactive session constructs
- 12:02Logical instants semantics
- 14:53Typing extensions
- 16:42Progress guarantees
- 18:07Contributions summary
- 19:30Open problems & future work
- 20:12Q&A
related talks
24mThread-Safe Reactive Programming
28mReactive Programming on the Bare Metal:A Formal Model for a Low-Level Reactive Virtual Machin
46mFunctional Reactive Programming
34mReactive Architecture
01h 11mReactive Architecture Patterns Debate
03mAm I only streaming? Thinking reactive
01h 28mIntroduction to Reactive Programming
29mAbout Combining Functional Reactive Programming and Replicated Data Types