ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Mon 19 Sep 2016 11:35 - 12:00 at Noh Theater - Session 1 Chair(s): Akimasa Morihata

We develop the operational semantics of an untyped probabilistic $\lambda$-calculus with continuous distributions, and both hard and soft constraints,as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics oλ-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integration over the space of traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language, or for a language with soft constraints.

Mon 19 Sep

 10:45 - 12:25: Research Papers - Session 1 at Noh Theater Chair(s): Akimasa MorihataUniversity of Tokyo, Japan 10:45 - 11:10Talk Farms, Pipes, Streams and Reforestation: Reasoning about Structured Parallel Processes using Types and HylomorphismsDavid CastroUniversity of St. Andrews, UK, Kevin HammondUniversity of St. Andrews, UK, Susmit SarkarUniversity of St. Andrews, UK DOI 11:10 - 11:35Talk Dag-Calculus: A Calculus for Parallel ComputationUmut AcarCarnegie Mellon University, Arthur CharguéraudInria, France, Mike RaineyInria, France, Filip SieczkowskiInria, France DOI 11:35 - 12:00Talk A Lambda-Calculus Foundation for Universal Probabilistic ProgrammingJohannes BorgströmUppsala University, Sweden, Ugo Dal LagoUniversity of Bologna, France, Andrew D. GordonMicrosoft Research, UK, Marcin SzymczakUniversity of Edinburgh, UK DOI 12:00 - 12:25Talk Deriving a Probability Density Calculator (Functional Pearl)Wazim Mohammed IsmailIndiana University, USA, Chung-chieh ShanIndiana University, USA DOI