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

lafi-2019
16:00 - 17:30: LAFI (né PPS) - D at Sala VI
lafi-201916:00 - 16:30
Talk
Simon Castellan, Hugo PaquetUniversity of Cambridge
lafi-201916:30 - 17:00
Talk
Steven HoltzenUniversity of California, Los Angeles, Joe QianUniversity of California, Los Angeles, Todd MillsteinUniversity of California, Los Angeles, Guy Van den BroeckUniversity of California, Los Angeles
lafi-201917:00 - 17:30
Talk
Matthew HeimerdingerIndiana University, Chung-chieh ShanIndiana University, USA