@String{j-jucs = "Journal of Universal Computer Science"}
@Article{Coquand:jucs_11_12:formal_topotoly_and_constructive,
  author =     "T. Coquand and B. Spitters",
  title =      "Formal {T}opology and {C}onstructive {M}athematics: the {G}elfand and {S}tone-{Y}osida {R}epresentation {T}heorems",
  abstract =   "We present a constructive proof of the   Stone-Yosida representation theorem for Riesz spaces motivated by   considerations from formal topology. This theorem is used to derive   a representation theorem for f-algebras. In turn, this theorem   implies the Gelfand representation theorem for C*-algebras of   operators on Hilbert spaces as formulated by Bishop and Bridges. Our   proof is shorter, clearer, and we avoid the use of approximate   eigenvalues.",
  journal =    j-jucs,
  year =       "2005",
  volume =     "11",
  number =     "12",
  pages =      "1932--1944",
  note =       "\url|http://www.jucs.org/jucs_11_12/formal_topotoly_and_constructive|"}