Beyond Types for Dyadic Interaction

on YouTube ↗01h 27m

" summary

Chronicles the 30-year path from Honda’s dyadic session types to multiparty session types and a linear logic correspondence that explains duality and resource discipline, explains why name passing breaks simple encodings and how projection and endpoint projection invariance must be reformulated to restore subject reduction, and reports practical outcomes: API generators for Java and Go, W3C standardization experiments applied to SMTP-like specs, and scaling to distributed systems showing the theory both finds subtle counterexamples and enables verified protocol implementations.

AI-written summary · about

" chapters (10)

1. 0:00Welcome
2. 8:13Session types and linear logic
3. 21:24Session types examples
4. 33:29Encoding session types
5. 47:21History of session types
6. 53:47Projecting session types
7. 59:33Five key topics
8. 1:06:32Subtyping and determinism
9. 1:16:52Future research directions
10. 1:24:21Expanding the community