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

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