\input zb-basic
\input zb-ioport
\iteman{io-port 06076966}
\itemau{Morgan, Carroll}
\itemti{Elementary probability theory in the Eindhoven style.}
\itemso{Gibbons, Jeremy (ed.) et al., Mathematics of program construction. 11th international conference, MPC 2012, Madrid, Spain, June 25--27, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31112-3/pbk). Lecture Notes in Computer Science 7342, 48-73 (2012).}
\itemab
Summary: We extend the Eindhoven quantifier notation to elementary probability theory by adding ``distribution comprehensions'' to it. Even elementary theories can be used in complicated ways, and this occurs especially when reasoning about computer programs: an instance of this is the multi-level probabilistic structures that arise in probabilistic semantics for security. Our exemplary case study in this article is therefore the probabilistic reasoning associated with a quantitative noninterference semantics based on Hidden Markov Models of computation. But we believe the proposal here will be more generally applicable than that, and so we also revisit a number of popular puzzles, to illustrate the new notation's wider utility.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-31113-0\_5}
\end