Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

Explore a 20-minute conference talk from POPL 2024 that introduces Clutch, a higher-order probabilistic relational separation logic supporting asynchronous probabilistic couplings. Delve into the development of a logical step-indexed logical relation for reasoning about contextual refinement and equivalence in higher-order programs with probabilistic choice, higher-order local state, and impredicative polymorphism. Learn how this approach addresses the limitations of traditional coupling rules in relational program logics by eliminating the need to synchronize sampling statements. Examine case studies demonstrating the practical applications of Clutch, and discover how all results have been formalized using the Coq proof assistant with the Coquelicot library and Iris separation logic framework.