Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 17:00 - 17:30 at Sala VI - D

We reason about measure equality by asserting axioms in Coq. The axioms constitute a small embedded monadic DSL, with standard primitives for random choice and scoring, and with intuitive equalities such as distributing random choices and multiplying scores. The axioms are only sound under the assumption that all functions are measurable and all measures are s-finite. Combined with inductive types and proofs, the axioms allow us to prove the correctness of probabilistic program transformations (including simplification and disintegration) and sampling techniques (including importance sampling and sequential Monte Carlo).

Tue 15 Jan

Displayed time zone: Belfast change

16:00 - 17:30
16:00
30m
Talk
Probabilistic Programming Inference via Intensional Semantics
LAFI
Simon Castellan , Hugo Paquet University of Cambridge
16:30
30m
Talk
Factorized Exact Inference for Discrete Probabilistic Programs
LAFI
Steven Holtzen University of California, Los Angeles, Joe Qian University of California, Los Angeles, Todd Millstein University of California, Los Angeles, Guy Van den Broeck University of California, Los Angeles
17:00
30m
Talk
Verified Equational Reasoning on a Little Language of Measures
LAFI
Matthew Heimerdinger Indiana University, Chung-chieh Shan Indiana University, USA