PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Wed 18 Jun 2025 11:10 - 11:30 at Cosmos, Violet & Tulip - Probabilistic Programming

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 Jun

Displayed time zone: Seoul change

10:30 - 12:10
Probabilistic ProgrammingPLDI Research Papers at Cosmos, Violet & Tulip
10:30
20m
Talk
Random Variate Generation with Formal Guarantees
PLDI Research Papers
Feras Saad Carnegie Mellon University, Wonyeol Lee POSTECH
DOI
10:50
20m
Talk
Semantics of Integrating and Differentiating Singularities
PLDI Research Papers
Jesse Michel Massachusetts Institute of Technology, Wonyeol Lee POSTECH, Hongseok Yang KAIST; IBS
DOI
11:10
20m
Talk
Probabilistic Refinement Session Types
PLDI Research Papers
Qiancheng Fu Boston University, Ankush Das Boston University, Marco Gaboardi Boston University
DOI
11:30
20m
Talk
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
20m
Talk
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