reference request : constructive measure theory As the title said, I would like to know if constructive measure theory has been developed somewhere ?
I am more precisely interested in the (constructive) theory of completely continuous valuation on locale, or eventually in countably continuous valuation on locale.
I know how to do constructively the integration of positive lower semi-continuous function with respect to a positive valuation (with value in lower semi-continuous real number) and I want to know if this kind of things has already been written properly somewhere (in order to be quoted) ?
On a closely related subject, I also want to know if the fact that the set of projection of an abelian von-neuman algebra $A$ is a frame whose corresponding locale $NSp A$ is the classifying space of the theory of normal character of $A$ and that complex valued function on $NSp A$ can be identified with unbounded operator affiliated to $A$ has been already written properly somewhere ? (I often see these mentioned in article or on MO, but I have never see a 'quotable' proof published. )
PS : By 'constructively' I mean using intuitionist logic.
Thank you !
 A: 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.
A: Thierry Coquand and Bas Spitters have several papers on this topic, see Integrals and Valuations, and Metric Boolean Algebras and Constructive Measure Theory.
A: 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.
A: An interesting recent possibility is in the work by Sam Sanders here in weak logical frameworks, inspired by the work of Simpson and Yokoyama.
