Fri 25 Oct 2024 12:00 - 12:20 at Pasadena - Probabilistic Programming and Analysis 2 Chair(s): Xin Zhang

We present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running time of deterministic programs, we introduce a novel notion of probabilistic cost credit. Probabilistic cost credits are a separation logic resource that can be used to pay for the cost of operations in programs, and that can be distributed across all possible branches of sampling instructions according to their weight, thus enabling us to reason about expected cost. The representation of cost credits as separation logic resources gives Tachis a great deal of flexibility and expressivity. In particular, it permits reasoning about amortized expected cost by storing excess credits as potential into data structures to pay for future operations. Tachis further supports a range of costs models, including running time and entropy usage. We showcase the versatility of this approach by applying our techniques to prove upper bounds on the expected cost of a variety of probabilistic algorithms and data structures, including randomized quicksort, hash tables, and meldable heaps. All of our results have been mechanized using Coq, Iris, and the Coquelicot real analysis library.

Fri 25 Oct

Displayed time zone: Pacific Time (US & Canada) change

11:00 - 12:20
Probabilistic Programming and Analysis 2OOPSLA 2024 at Pasadena
Chair(s): Xin Zhang Peking University
11:00
20m
Talk
Programmable MCMC with Soundly Composed Guide Programs
OOPSLA 2024
Long Pham Carnegie Mellon University, Di Wang Peking University, Feras Saad Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
DOI
11:20
20m
Talk
Quantitative Bounds on Resource Usage of Probabilistic Programs
OOPSLA 2024
Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Tobias Meggendorfer Lancaster University, UK (Leipzig Campus), Đorđe Žikelić Singapore Management University, Singapore
DOI
11:40
20m
Talk
Sensitivity by ParametricityOOPSLA 2024 Distinguished Artifact Award
OOPSLA 2024
Elisabet Lobo-Vesga DPella AB, Carlos Tomé Cortiñas Chalmers University of Technology, Alejandro Russo Chalmers University of Technology, Sweden / University of Gothenburg, Sweden / DPella AB, Sweden, Marco Gaboardi Boston University
DOI
12:00
20m
Talk
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
OOPSLA 2024
Philipp G. Haselwarter Aarhus University, Kwing Hei Li Aarhus University, Markus de Medeiros New York University, Simon Oddershede Gregersen New York University, Alejandro Aguirre Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
DOI Pre-print