reference request : constructive measure theory

Thierry Coquand and Bas Spitters have several papers on this topic, see Integrals and Valuations, and Metric Boolean Algebras and Constructive Measure Theory.

Steve Vickers’ A monad of valuation locales presents a strong monad on the category of locales, a localic analogue of the Giry monad. It is commutative, i.e. product valuations exist and a Fubini Theorem holds. Concrete representations are given for the tensor product of lattices and for the modular monoid. Vickers combines domain theoretic measure theory with insights from our paper above. His theory is geometric. One difference with our work is that we focus on valuations on compact regular locales which give integrals to the Dedekind reals, whereas in the general theory the integrals are only lower reals.

You'll find some interesting work on this by Alex Simpson, as you can see by browsing around his web page. I also wrote a blog entry on Simpson's work on the space of random sequences.