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

We extend a stream-processing programming language, whose denotational semantics is given using the domain of streams, so that it can support probabilistic action. We give a denotational semantics to the extended language (which we call SProcP). We take the domain of probability distributions over streams as the denotational domain; it constitutes a cpo according to Saheb-Djaromi [3].

This work is motivated by the second author’s recent hybrid-system verification work [4]. In this work, we used nonstandard analysis [1] to the denotational semantics of a stream-processing language so that it accommodates infinitesimal values. The extended language can express continuous signals and computation on them. We plan to do the same extension to the current language to obtain a language for processing probabilistic continuous-time signal.

The extension is for the most part straightforward. A tricky part is the denotation of binary operations e1 + e2. Since the denotation of the expressions e1 and e2 are in general not independent from each other, we cannot write define its denotation using those of e1 and e2. Our current definition is to assume an opaque function that gives a joint distribution of the denotations of e1 and e2. If we can reason that e1 is independent from e2 (by some program analysis), the denotation of e1 + e2 can be given in more explicit way.

[3] N. Saheb-Djahromi. Cpo’s of measures for nondeterminism. Theor. Comput. Sci., 12:19–37, 1980.

[4] K. Suenaga, H. Sekine, and I. Hasuo. Hyperstream processing systems: nonstandard modeling of continuous-time signals. In POPL 2013, pages 417–430, 2013.

[5] A. Robinson. Non-standard analysis. Studies in logic and the foundations of mathematics. North-Holland Pub. Co., 1966. URL https://books.google.co.jp/books?id=-eJLAAAAMAAJ.

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