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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

15:30 - 16:30: Poster SessionPPS at Room St Petersburg II
15:30 - 16:30
Meeting
PPS
Aleksey KligerXamarin, Inc., Sean StromstenBAE Systems, Inc.
Pre-print
15:30 - 16:30
Meeting
PPS
Theophilos GiannakopoulosBAE Systems, Inc., Mitchell WandNortheastern University, Andrew CobbNortheastern University
Pre-print
15:30 - 16:30
Meeting
PPS
Larry MossIndiana University, Chung-chieh ShanIndiana University, Alexandra SilvaRadboud University Nijmegen
Pre-print
15:30 - 16:30
Meeting
PPS
Faris Abou-SalehUniversity of Oxford, Kwok-Ho CheungUniversity of Oxford, Jeremy GibbonsUniversity of Oxford, UK
Pre-print
15:30 - 16:30
Meeting
PPS
Johannes HölzlTechnische Universität München
Pre-print
15:30 - 16:30
Meeting
PPS
Yohei MiyamotoGraduate School of Informatics, Kyoto University, Kohei Suenaga, Koji NakazawaGraduate School of Information Science, Nagoya University
Pre-print
15:30 - 16:30
Meeting
PPS
Ryan CulpepperNortheastern University
Pre-print
15:30 - 16:30
Meeting
PPS
Pre-print
15:30 - 16:30
Meeting
PPS
Adam ŚcibiorUniversity of Cambridge, Andrew D. GordonMicrosoft Research and University of Edinburgh
Pre-print
15:30 - 16:30
Meeting
PPS
Adam ŚcibiorUniversity of Cambridge, Bernhard SchölkopfMPI Tuebingen
Pre-print