VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs

We introduce a Hoare-style logic for probabilistic programs, called VPHL, that has been formally verified in the Coq proof assistant. VPHL features propositional, rather than additive, assertions and a simple set of rules for reasoning about these assertions using the standard axioms of probability theory. VPHL's assertions are partial correctness assertions, meaning that their conclusions are dependent upon (deterministic) program termination. The underlying simple probabilistic imperative language, PrImp, includes a probabilistic toss operator, probabilistic guards and potentially-non-terminating while loops.