ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Tue 14 Apr 2015 12:00 - 12:30 at Skeel - Session 1 Chair(s): Jan Vitek

Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a probabilistic functional language. In this work, we implement such a compiler for a modified version of this language within the theorem prover Isabelle and give a formal proof of its soundness w.r.t. the semantics of the source and target language. Together with Isabelle’s code generation for inductive predicates, this yields a fully verified, executable density compiler.

Tue 14 Apr

10:30 - 12:30: ESOP - Session 1 at Skeel
Chair(s): Jan VitekNortheastern University
esop-2015-papers10:30 - 11:00
Andrew D. GordonMicrosoft Research and University of Edinburgh, Claudio RussoMicrosoft Research, Marcin SzymczakUniversity of Edinburgh, Johannes BorgströmUppsala University, Nicolas RollandMicrosoft Research, Thore GraepelMicrosoft Research, Daniel TarlowMicrosoft Research
esop-2015-papers11:00 - 11:30
Tie ChengCNRS, ENS, INRIA, Paris, France, Xavier RivalINRIA/CNRS/ENS Paris
esop-2015-papers11:30 - 12:00
Neil TorontoBrigham Young University, Jay McCarthy, David Van Horn
esop-2015-papers12:00 - 12:30
Manuel EberlTechnische Universität München, Johannes HölzlTechnische Universität München, Tobias NipkowTechnische Universität München