Approximate Relational Reasoning for Higher-Order Probabilistic Programs
summary
Describes Approxis, a higher-order separation logic that treats error credits as first-class resources to prove approximate program refinements for an ML-like language with discrete sampling, higher-order state and functions. Development is mechanized in Coq on top of Iris, includes a logical-relation model that quantifies over credits to get exact contextual equivalence, and verifies concrete results: PRP/PRF switching, IND-CPA encryption bounds, rejection samplers and efficient B‑tree samplers, plus new coupling and sampling rules.
AI-written summary · about