Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a 20-minute conference talk from PLDI 2023 that introduces Zar, a formally verified compiler pipeline for discrete probabilistic programs. Learn how Zar translates programs with unbounded loops in the conditional probabilistic guarded command language (cpGCL) into proved-correct executable samplers using the random bit model. Discover the key concept of reducing all discrete probability distributions to unbiased coin-flipping schemes. Examine the compilation process, including the translation to choice-fix trees and coinductive interaction trees. Understand the sampling equidistribution theorem that establishes the correctness of compiled samplers. Gain insights into the implementation and verification in Coq, as well as the extraction of verified samplers to OCaml and Python. See empirical validations on illustrative examples and explore the available artifacts evaluated as reusable.
Syllabus
[PLDI'23] Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning
Taught by
ACM SIGPLAN
Related Courses
CompilersStanford University via edX Build a Modern Computer from First Principles: Nand to Tetris Part II (project-centered course)
Hebrew University of Jerusalem via Coursera Compiler Design
Indian Institute of Technology, Kharagpur via Swayam Foundations to Computer Systems Design
Indian Institute of Technology Madras via Swayam Compiler Design
YouTube