YoVDO

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

Offered By: ACM SIGPLAN via YouTube

Tags

Formal Methods Courses Asynchronous Programming Courses Probabilistic Programming Courses Coq Courses

Course Description

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!
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.

Syllabus

[POPL'24] Asynchronous Probabilistic Couplings in Higher-Order Separation Logic


Taught by

ACM SIGPLAN

Related Courses

Verifying the LLVM
Strange Loop Conference via YouTube
Beweisbar sichere Software
media.ccc.de via YouTube
RustBelt: A Quick Dive Into the Abyss - Formalizing Rust's Safety Story
Rust via YouTube
Building Measure Theory Using Hierarchy Builder
Hausdorff Center for Mathematics via YouTube
Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015
GOTO Conferences via YouTube