Probabilistic Refinement Session Types
summary
Introduces probabilistic refinement session types and implements a prototype PReST prototype in OCaml with a bi-directional type checker that emits nonlinear real arithmetic constraints solved by SMT solver (Z3); CVC5 proves less robust. Supports symbolic probabilities (types indexed by p), probabilistic and regular choice, and a flip primitive; integrates cost annotations to give expected recursion-depth bounds. Proves type safety, global progress, probability consistency, and an expected-cost theorem; benchmarks across four categories scale and typically solve within 0.3s.
AI-written summary · about
chapters (11)
- 0:00Probabilistic refinement session types
- 1:51Randomized distributed algorithms
- 3:16PRESS language core
- 6:47Type checking probabilistic channels
- 9:14Modeling distributions in PRESS
- 13:11Verifying uniform distribution
- 15:45Crowd forwarding protocol
- 17:35PRESS meta-theory
- 18:16Type checker implementation
- 20:26Future work
- 21:52Q&A
related talks
23mPrecise Subtyping for Asynchronous Multiparty Sessions
16mPomsets with Preconditions: A Simple Model of Relaxed Memory
20mTruly Stateless, Optimal Dynamic Partial Order Reduction
50mSession Types Meet Polymorphism and Dependent Types
21mFair Termination of Binary Sessions
23mProbabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and(…)
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
31mTermination in Concurrency, Revisited