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
Times are displayed in time zone: (GMT+01:00) Greenwich Mean Time : Belfast change

16:00 - 17:30: LAFI (né PPS) - D at Sala VI
lafi-201916:00 - 16:30
Simon Castellan, Hugo PaquetUniversity of Cambridge
lafi-201916:30 - 17:00
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
Matthew HeimerdingerIndiana University, Chung-chieh ShanIndiana University, USA