Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning
summary
Zar compiles cpGCL programs with unbounded loops and conditioning into proved-correct samplers in the random bit model, implemented and fully verified in Coq and extracted to OCaml and Python; correctness is a formal equidistribution theorem showing samples match the cwp semantics. The pipeline builds choice-fix trees, debiases rational probabilities into unbiased coin-flip schemes (using rejection loops), and targets coinductive interaction trees for execution. Artifacts are available and evaluated; performance is competitive on many examples but drops with low-probability conditioning; proofs use classical axioms (indefinite description, excluded middle).
AI-written summary · about