Event-Driven Multiparty Session Actors

on YouTube ↗35m

" summary

Claims a first statically-typed multiparty session system for actors that lets a single actor participate in multiple sessions by combining flow-sensitive effect typing with first-class event handlers. Delivers a small core calculus, two typing judgments (value and flow-sensitive computation with session pre/postconditions), a type preservation proof, and a prototype typechecker plus small-step interpreter; Scala API generation is underway. Limits: global progress and fidelity proofs are pending and session-switching currently requires suspension.

AI-written summary · about

" chapters (27)

1. 0:00Introduction and speaker welcome
2. 0:23Talk overview and motivation
3. 1:04Actor languages and their challenges
4. 3:11Multi-party session typing basics
5. 5:42Two-buyer protocol walkthrough
6. 8:11Challenges applying session types to actors
7. 9:15Historical approaches to session-typed actors
8. 10:18Flow-sensitive effect typing for session typing
9. 11:44Key idea: Event-driven multiparty session actors
10. 13:28Core components of the programming model
11. 15:59Formal core calculus and typing rules
12. 21:45Operational semantics and meta-theory
13. 22:48Implementation status and future work
14. 23:09Summary and contributions
15. 23:53Q&A: Distinction between event and effect handlers
16. 24:57Q&A: Implementing schedulers with effect handlers
17. 26:01Q&A: Comparison with asynchronous effects work
18. 27:08Q&A: Access point declaration and inference
19. 28:52Q&A: Session type declaration challenges
20. 29:13Q&A: Avoiding effect handler machinery
21. 29:35Q&A: Monitoring approach for session types
22. 30:42Q&A: Fault tolerance in this setting
23. 31:49Q&A: Exception handling in effect systems
24. 32:10Q&A: Fault tolerance and replication
25. 32:30Q&A: Session typing with hot code reloading
26. 33:34Q&A: Why first-class event handlers
27. 33:56Q&A: Handlers as values vs computations

" related talks

• 15mA Multiparty Session Typing Discipline for Fault-tolerant Event-driven Distributed ProgrammingPatrick Eugster, Raymond Hu, Lukasz Ziarek, Malte Viering · OOPSLA 2021
• 23mA Synthetic Reconstruction of Multiparty Session TypesSung-Shik Jongmans, Francisco Ferreira, David Castro-Perez · POPL 2026
• 32mMulticompatibility for Multiparty-Session CompositionNobuko Yoshida, Lorenzo Gheri, Franco Barbanera, Mariangiola Dezani · PPDP 2023
• 37mSession Types: A History and ApplicationsNobuko Yoshida · Code Mesh LDN 2020
• 37mUsing Event Structures to model Multiparty Session Types: results and open problemsPaola Giannini, Ilaria Castellani · ST30 2023
• 45mTaming Distribution: Formal Protocols for Akka TypedRoland Kuhn · Scala Days Copenhagen 2017
• 18mHybrid Multiparty Session Types: Compositionality for Protocol Specification th...Nobuko Yoshida, Lorenzo Gheri · OOPSLA 2023
• 15mStatically Verified Refinements for Multiparty ProtocolsNobuko Yoshida, Raymond Hu, Fangyi Zhou, Francisco Ferreira, Rumyana Neykova · OOPSLA 2020