This program is tentative and subject to change.
Session types provide a formal type system to define and verify communication protocols between message-passing processes. In order to analyze randomized systems, recent works have extended session types with probabilistic type constructors. Unfortunately, all the proposed extensions only support constant probabilities which limits their applicability to real-world systems. Our work addresses this limitation by introducing probabilistic refinement session types which enable symbolic reasoning for concurrent probabilistic systems in a core calculus we call PReST. The type system is carefully designed to be a conservative extension of refinement session types and supports both probabilistic and regular choice type operators. We also implement PReST in a prototype which we use for validating probabilistic concurrent programs. The added expressive power leads to significant challenges, both in the meta theory and implementation of PReST, particularly with type checking: it requires reconstructing intermediate types for channels when type checking probabilistic branching expressions. The theory handles this by semantically quantifying refinement variables in probabilistic typing rules, a deviation from standard refinement type systems. The implementation relies on a bi-directional type checker that uses an SMT solver to reconstruct the intermediate types minimizing annotation overhead and increasing usability. To guarantee that probabilistic processes are almost-surely terminating, we integrate cost analysis into our type system to obtain expected upper bounds on recursion depth. We evaluate PReST on a wide variety of benchmarks from 4 categories: (i) randomized distributed protocols such as Itai and Rodeh's leader election, bounded retransmission, etc., (ii) parametric Markov chains such as random walks, (iii) probabilistic analysis of concurrent data structures such as queues, and (iv) distributions obtained by composing uniform distributions using operators like max, and sum. Our experiments show that the PReST type checker scales to large programs with sophisticated probabilistic distributions.
This program is tentative and subject to change.
Wed 18 JunDisplayed time zone: Seoul change
10:30 - 12:10 | |||
10:30 20mTalk | Random Variate Generation with Formal Guarantees PLDI Research Papers DOI | ||
10:50 20mTalk | Semantics of Integrating and Differentiating Singularities PLDI Research Papers DOI | ||
11:10 20mTalk | Probabilistic Refinement Session Types PLDI Research Papers DOI | ||
11:30 20mTalk | Stochastic Lazy Knowledge Compilation for Inference in Discrete Probabilistic Programs PLDI Research Papers Maddy Bowers Massachusetts Institute of Technology, Alexander K. Lew Massachusetts Institute of Technology; Yale University, Joshua B. Tenenbaum Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology DOI | ||
11:50 20mTalk | Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic Programming PLDI Research Papers Cameron Moy Northeastern University, Jack Czenszak Northeastern University, John Li Northeastern University, Brianna Marshall Northeastern University, Steven Holtzen Northeastern University DOI |