Write a Blog >>
Sat 23 Jan 2016 15:30 - 16:30 at Room St Petersburg II - Poster Session

The goal of this paper is to advertise the application of fixed points and ω-complete partial orders (ω-cpos) in the formalization and analysis of probabilistic programming languages. The presented work is formalized in the Isabelle theorem prover.

By applying ω-cpos to the analysis of MDPs we get a nice theory of fixed points. This allows us to transfer least and greatest fixed points through expectation on Markov chains and maximal and minimal expectation on MDPs. One application is to define the operational semantics of pGCL by MDPs, e.g. relating the denotational and operational semantics of pGCL is now a matter of fixed point equations and induction.

Note: After acceptance I discovered that large parts of the presented work were already developed by Monniaux [1]. Still, the main contribution of the presented work is the formalization in the interactive theorem prover Isablle/HOL.

[1] David Monniaux: Abstract interpretation of programs as Markov decision processes

Sat 23 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

15:30 - 16:30
Poster SessionPPS at Room St Petersburg II
15:30
60m
Meeting
Insomnia: Types and Modules for Probabilistic Programming
PPS
Aleksey Kliger Xamarin, Inc., Sean Stromsten BAE Systems, Inc.
Pre-print
15:30
60m
Meeting
Finite-depth Higher-order Abstract Syntax Trees for Reasoning about Probabilistic Programs
PPS
Theophilos Giannakopoulos BAE Systems, Inc., Mitchell Wand Northeastern University, Andrew Cobb Northeastern University
Pre-print
15:30
60m
Meeting
Coalgebraic Trace Semantics for Probabilistic Processes: Preliminary Proposal
PPS
Larry Moss Indiana University, Chung-chieh Shan Indiana University, Alexandra Silva Radboud University Nijmegen
Pre-print
15:30
60m
Meeting
Reasoning about Probability and Nondeterminism
PPS
Faris Abou-Saleh University of Oxford, Kwok-Ho Cheung University of Oxford, Jeremy Gibbons University of Oxford, UK
Pre-print
15:30
60m
Meeting
Fixed Points for Markov Decision Processes
PPS
Johannes Hölzl Technische Universität München
Pre-print
15:30
60m
Meeting
A Denotational Semantics of a Probabilistic Stream-Processing Language
PPS
Yohei Miyamoto Graduate School of Informatics, Kyoto University, Kohei Suenaga , Koji Nakazawa Graduate School of Information Science, Nagoya University
Pre-print
15:30
60m
Meeting
Observation Propagation for Importance Sampling with Likelihood Weighting
PPS
Ryan Culpepper Northeastern University
Pre-print
15:30
60m
Meeting
Problems of the Lightweight Implementation of Probabilistic Programming
PPS
Pre-print
15:30
60m
Meeting
Parameterized Probability Monad
PPS
Adam Ścibior University of Cambridge, Andrew D. Gordon Microsoft Research and University of Edinburgh
Pre-print
15:30
60m
Meeting
Reproducing Kernel Hilbert Space Semantics for Probabilistic Programs
PPS
Adam Ścibior University of Cambridge, Bernhard Schölkopf MPI Tuebingen
Pre-print