BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Verified Compiler for Probability Density Functions  - Tobias Ni
 pkow\, Institute of Informatics Technical Institute of Munich
DTSTART:20140724T090000Z
DTEND:20140724T100000Z
UID:TALK53509@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Bhat\, Borgström\, Gordon and Russo recently published a comp
 iler from a small probabilistic functional programming language to probabi
 lity density functions. That is\, the input is a functional program that g
 enerates random values according to some distribution. The compiler transl
 ates the program into its probability density function (if it exists). In 
 this talk we present a formalization of this work in the interactive theor
 em prover Isabelle/HOL\, including a verification of the compiler.
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR