lo.logic - Coherent spaces

In Proofs and Types, Girard discusses coherent (or coherence) spaces, which is defined as a set family which is closed downward ($ain A,bsubseteq aRightarrow bin A$), and binary complete (If $Msubseteq A$ and $forall a_1,a_2in M (a_1cup a_2in A)$, then $cup Min A$)

It was informally related to topological spaces. Anyway, I have a couple pretty general questions:
Are they particularly useful outside of type theory? Perhaps more specifically, do coherent spaces show up in topology?

The last one raises up a philosophical question I've been pondering: Why is it that some structures seem to show up all over the place, while others that seem like they "should" be more or less equivalently useful don't seem to show up much at all? An example would be matroids versus topologies. I feel, morally, that matroids should be more useful than they seem to be.

The last question probably doesn't have any sort of solid answer, but it would be nice to hear some thought from people with a stronger background.

Cheers and thanks,
Cory

Edit:
After thinking about this some more, it has occurred to me that coherent spaces are a sort of "dual" to ultrafilters. I really don't have the background to be terribly formal, but, let me try to explain:

Let $(X,C)$ be a coherent space, and call the elements of $C$ "open" (I think the analogy is justified, because adding $X$ to $C$ makes it a topology), then the closed sets form an ultrafilter. The one problem is that the closure under intersection is a bit strong (the set of closed sets is closed under arbitrary intersections).
On the other hand, if $(X,U)$ is an ultrafilter, the set of complements of open sets almost forms a coherent space-- but the conditions on unions is just a little too weak.

So, my next question is: Has this link been explored at all? Is there even anything there to explore?

Thanks again.