Probabilistic Resource-Aware Session Types

on YouTube ↗26m

" summary

Extends binary session types to describe message probability distributions and to infer expected-resource bounds automatically, using a type reconstruction algorithm that reduces inference to linear constraint solving and LP solving, with linear-time type checking. Key theory is probabilistic session types and a nested multiverse semantics that avoids unsound global distributions. The NomosPro implementation infers probabilities and costs, produces a symbolic 1.25·n bound at 20% drop, verifies a Markov chain with 64 states and 420 transitions, and scales to two broadcast and a bounded-retransmission protocol.

AI-written summary · about

" chapters (11)

1. 0:00Start
2. 1:04Many Concurrent Systems are Probabilistic
3. 3:53Probabilistic Reasoning with Session Types
4. 4:25Applications of Probabilistic Reasoning
5. 5:12Without Probability, Cost is Worst-Case
6. 6:18What's in the Paper?
7. 7:37Probabilistic Process Expressions
8. 12:38Nested Multiverse Semantics of Nomos Pro 12
9. 13:41Bounded Retransmission Protocol
10. 18:25Expected Number of State Transitions
11. 19:31Conclusion