Bas Spitters
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 noncommutative integration theory  the foundations of quantum mechanics.
