t ::= c | c -> t | c /\ (c -> t)
where c ranges over constraints, /\ is conjunction and -> intuitionistc implication. We motivate why it is interesting to consider as observable a "causality" relation on the store: what is observed is not just the conjunction of constraints deposited in the store, but also the causal dependencies between these constraints - what constraints were required to be present in the computation before others could be generated. We show that the same construction used to give the "interleaving" semantics in [SRP91] can be used to give a true-concurrency semantics provided that denotations are taken to be sets of bounded closure operators, which can be generated via the grammar:
k ::= c | c -> k | k /\ k
Thus we obtain a denotational semantics for CCP fully-abstract with respect to observing this "causality" relation on constraints. This semantics differs from the earlier semantics in preserving more fine-grained structure of the computation; in particular the law
(c -> A) /\ (d -> B) = (c -> (A /\ (d -> B))) [] (d -> (B /\ (c -> A)))
is not verified ([] is indeterminate choice). Relationships between such a denotational approach to true concurrency and different powerdomain constructions are explored.