POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 15:35 - 16:00 at Amphitheater 44 - Probabilistic Programming Chair(s): Marco Gaboardi

Couplings are a powerful tool for proving rapid mixing of probabilistic processes, with applications across many fields of mathematics and computer science. A recent development in formal verification identifies a close connection between couplings and pRHL, a relational program logic motivated by applications to provable security. This close connection opens the door to using the program logic pRHL far beyond its envisioned scope, for verifying examples from the coupling literature. However, there is a technical challenge: whereas many applications of coupling requires reasoning about the coupled process, every derivation in pRHL merely proves its existence. Moreover, pRHL is inherently incomplete, and as a consequence, is not able to capture some advanced forms of couplings such as shift couplings. We address both problems as follows.

First, we define a proof-relevant program logic, called prpRHL, which makes explicit the coupling in a pRHL derivation, in the form of a product program that simulates two correlated runs of the original program. Existing verification tools for probabilistic programs can then be directly applied to the probabilistic product to prove quantitative properties of the coupling, for instance, for analyzing the speed of convergence of the probabilistic process.

Second, we equip prpRHL with a powerful rule for While loops, in which one can freely interleave synchronized and unsynchronized loop iterations. Our proof rule is sufficiently expressive to capture examples of shift couplings, and is relatively complete for deterministic programs.

We show soundness of prpRHL and use it to analyze two classes of examples. The first class of examples considers rapid mixing using different tools from coupling: standard coupling, shift coupling, and path coupling, a compositional principle for combining local couplings into a global coupling. The second class of examples proves (approximate) equivalence between a source and an optimized program, for several instances of loop optimizations from the literature.

Wed 18 Jan

POPL-2017-papers
14:20 - 16:00: POPL - Probabilistic Programming at Amphitheater 44
Chair(s): Marco GaboardiSUNY Buffalo, USA
POPL-2017-papers14:20 - 14:45
Talk
Leonidas LampropoulosUniversity of Pennsylvania, Diane Gallois-WongInria Paris, ENS Paris, Cătălin HriţcuInria Paris, John HughesChalmers University of Technology, Benjamin C. PierceUniversity of Pennsylvania, Li-yao XiaENS Paris
Pre-print
POPL-2017-papers14:45 - 15:10
Talk
Chung-chieh ShanIndiana University, USA, Norman Ramsey
Pre-print
POPL-2017-papers15:10 - 15:35
Talk
Krishnendu ChatterjeeIST Austria, Petr NovotnyIST Austria, Djordje ZikelicUniversity of Cambridge
POPL-2017-papers15:35 - 16:00
Talk