I always had trouble forming an intuition for coherence spaces, until I became more familiar with domain theory and read Girard's "The System F of variable types, fifteen years later". Coherence spaces are just a special kind of domain, and I found it much easier to understand what coherence means starting from there. I'll try to give an explanation that made more-or-less sense to me.
Imagine that you want to study programs that take integer inputs to integer outputs. In general, these programs may loop forever, so it makes sense to model them mathematically as partial functions from integers to integers: if the program loops, the corresponding partial function is undefined on that input. We can view such a partial function $f$ as a graph: a set of pairs of integers $(n, m)$ such that $f$ is defined on $n$ and equal to $m$. This allows us to represent these functions as a coherence space:
- The web of the coherence space is the set of pairs of integers $(n, m)$.
- Two pairs $(n, m)$ and $(n', m')$ are coherent if and only if $n$ and $n'$ are different, or $m$ and $m'$ are equal.
By unpacking definitions, we see that every clique of this coherence space is the graph of a partial functions, and vice versa. We can interpret the coherence relation as saying that, one a partial function is defined on an input, it produces only one result for that input. If you're used to other kinds of domain-theoretic semantics, inclusion of cliques corresponds to the usual Scott order on partial functions on integers.
Edit
The above example is actually a particular case of a more general construction on coherence spaces, which is used to represent functions on coherence spaces that behave somewhat like computable functions. This construction is described in Girard's paper mentioned above, though with a slightly different terminology.
Let's say that $X$ and $Y$ are coherence spaces. A stable function of type $X \to Y$ is a function from cliques of $X$ to cliques of $Y$ that satisfies the following two conditions:
- If $a \subseteq b$ are cliques of $X$, then $f(a) \subseteq f(b)$.
- If $(a_i)_{i \in I}$ is a nonempty directed family of cliques of $X$, then $f\left(\bigcup_i a_i\right) = \bigcup_i f(a_i)$. ("Directed" means that, for every $i, j \in I$, there is some $k \in I$ such that $a_i \subseteq a_j$ and $a_j \subseteq a_k$.)
- If $a \cup b$ is a clique of $X$, then $f(a \cap b) = f(a) \cap f(b)$.
This definition might look weird, but simple instances are much more familiar. Let us define the following coherence space $N$:
- The web of $N$ is the set of natural numbers $\mathbb{N}$.
- Two elements of the web are coherent if and only if they are equal.
The cliques of $N$ are either singletons $\{n\}$ or the empty set. Thus, we can show that a partial function of type $\mathbb{N} \to \mathbb{N}$ is the same thing as a stable function of type $N \to N$. More precisely, note that, in this case, the conditions 2 and 3 in the above definition are automatically satisfied. Thus, if $f : N \to N$ is a stable function, then we can define a partial function $g : \mathbb{N} \to \mathbb{N}$ by defining $g(n) = m$ if and only if $f(\{n\}) = \{m\}$. Conversely, we can show that any partial function $g$ corresponds uniquely to some stable function $f$.
One fundamental result about coherence spaces is that stable functions between them can be represented as coherence spaces. This is proved in Girard's paper (cf. Theorem 1.4), but here is a high-level overview. First, we can prove that every stable function $f : X \to Y$ is entirely determined by the set $F$ of pairs $(a, b)$ such that $a$ is a finite clique of $X$, $b \in f(a)$, and $b \notin f(a')$ for any $a' \subsetneq a$. Next, we define a coherence space $X \Rightarrow Y$ as follows:
The web $|X \Rightarrow Y|$ is the set $X_{\mathit{fin}} \times |Y|$, where $X_{\mathit{fin}}$ denotes the set of finite cliques of $X$.
Two pairs $(a, b)$ and $(a', b')$ are coherent if and only if either (1) $a = a'$ and $b = b'$; or (2) if $a \cup a'$ is a clique of $X$, then $b \neq b'$ and $b$ is coherent with $b'$.
Finally, we can show that the set of pairs $F$ constructed above is a clique of $X \Rightarrow Y$, and that every clique of $X \Rightarrow Y$ arises uniquely in this way.
In terms of the above example, when $X$ and $Y$ are $N$, the web of the coherence space consists of pairs of the form $(\{n\}, m)$, and we can show that two pairs $(\{n\}, m)$ and $(\{n'\}, m')$ are coherent if and only if either $n \neq n'$ or $m = m'$. This is essentially the definition of the coherence space of partial functions on natural numbers that we gave above.
