As an illustration of the use of proof mining we extract a constructive proof of the Riesz representation theorem out of the classical proof. This allows us to generalize the theorem to valuations on locales and to apply it in the context of non-commutative integration theory --- the foundations of quantum mechanics.

Another application is a convenient construction of the Giry monad which is important in the theory of stochastic processes and in the theory of probabilistic computations.