  The aim of this paper is to present an elementary computable theory of random
variables, based on the approach to probability via valuations. The theory is
based on a type of lower-measurable sets, which are controlled limits of open
sets, and extends existing work in this area by providing a computable theory
of conditional random variables. The theory is based within the framework of
type-two effectivity, so has an explicit direct link with Turing computation,
and is expressed in a system of computable types and operations, so has a clean
mathematical description.
