** ****Monday, ****February 8, 2010 **

4:00pm

5130 Upson Hall

**Abstract: **

## In this talk I will describe two complementary but equivalent
semantics for a high-level probabilistic programming language.
One of these interprets programs as continuous linear operators
on a space of measures. This is a "forward-moving"
semantics analogous to powerdomain transformers for nondeterministic
programs. The other is a measurable-function transformer semantics.
It is a "backward-moving" semantics analogous to predicate transformers.
The two semantics are dual in the sense of Stone duality.

I will then describe a logic based on these semantics called
PPDL. It is more arithmetic in nature than truth-functional,
thus it might better be called a calculus than a logic.
It satisfies a small model property and can be
decided in polynomial space, thus is amenable to model-checking.
I will give an example of its use in deriving

mechanically the expected length of a random walk.