Approximate Relational Reasoning for Higher-Order Probabilistic Programs

This conference talk from POPL 2025 presents Approxis, a higher-order approximate relational separation logic for reasoning about approximate equivalence of probabilistic programs. Explore how the researchers extend relational program logic to handle ML-like languages with discrete probabilistic sampling, higher-order functions, and higher-order state. The presentation introduces the novel concept of error credits in a relational setting, enabling more expressive modularity, composition, and new approximate relational rules. Learn about the logical relation model that quantifies over error credits to prove exact contextual equivalence. The research demonstrates practical applications through examples including the PRP/PRF switching lemma, IND$-CPA security of an encryption scheme, and rejection samplers. All results have been mechanized in the Coq proof assistant and the Iris separation logic framework, with artifacts available and functionally evaluated.