POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Fri 16 Jan 2026 14:25 - 14:50 at Nef - Probabilistic Programming Chair(s): Michele Pagani

Although randomization has long been used in distributed computing, formal methods for reasoning about probabilistic concurrent programs have lagged behind. No existing program logics can express specifications about the full distributions of outcomes resulting from programs that are both probabilistic and concurrent. To address this, we introduce Probabilistic Concurrent Outcome Logic (pcOL), which incorporates ideas from concurrent and probabilistic separation logics into Outcome Logic to introduce new compositional reasoning principles. At its core, pcOL reinterprets the rules of Concurrent Separation Logic in a setting where separation models probabilistic independence, so as to compositionally describe joint distributions over variables in concurrent threads. Reasoning about outcomes also proves crucial, as case analysis is often necessary to derive precise information about threads that rely on randomized shared state. We demonstrate pcOL on a variety of examples, including to prove almost sure termination of unbounded loops.

Fri 16 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

14:00 - 15:40
Probabilistic ProgrammingPOPL at Nef
Chair(s): Michele Pagani ENS Lyon
14:00
25m
Talk
Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
POPL
Sangho Lim KAIST, Hyoungjin Lim KAIST, Wonyeol Lee POSTECH, Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University, Hongseok Yang KAIST
DOI
14:25
25m
Talk
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and InvariantsDistinguished Paper
POPL
Noam Zilberstein Cornell University, Alexandra Silva Cornell University, Joseph Tassarotti New York University
DOI
14:50
25m
Talk
Probabilistic Programming with Vectorized Programmable InferenceRemote
POPL
McCoy Reynolds Becker MIT, Mathieu Huot MIT, George Matheos Massachusetts Institute of Technology, Xiaoyan Wang Massachusetts Institute of Technology, Karen Chung Massachusetts Institute of Technology, Colin Smith Massachusetts Institute of Technology, Sam Ritchie Massachusetts Institute of Technology, Rif A. Saurous Google, Alexander K. Lew Yale University, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI
15:15
25m
Talk
Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
POPL
Davide Barbarossa University of Bath, Paolo Pistone Université Claude Bernard Lyon 1
DOI