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

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