21 citations · 47 across the 7 of their papers we have counts for
4 papers · 1 filter
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre +3
Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational p…
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros +4
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…
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros +4
Probabilistic programs often trade accuracy for efficiency, and thus may, with a small probability, return an incorrect result. It is important to obtain precise bounds for the pro…
Almost-Sure Termination by Guarded Refinement
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter +2
Almost-sure termination is an important correctness property for probabilistic programs, and a number of program logics have been developed for establishing it. However, these logi…