I have just put on the web two papers that explore constructive localic (and also topos) aspects of Lawvere's generalized metric spaces (see TAC Reprints 1, "Metric spaces, generalized logic and closed categories"). My papers are: "Localic completion of generalized metric spaces I" "Localic completion of generalized metric spaces II: Powerlocales" They can both be found through http://www.cs.bham.ac.uk/~sjv/README.html Lawvere describes generalized metric spaces as categories enriched over the extended half line [0, infinity]. I replace this enrichment category by a locale with the same points, and show how to obtain a completion as a locale. Topos aspects include a proof that the generic localic completion is an opfibration in the 2-category of grothendieck toposes. My second paper shows how the powerlocales of the localic completions are themselves also localic completions, and uses this to analyse questions of compactness. Steve Vickers.