The paper is available here Interaction Categories and the Foundations of Typed Concurrent Programming Abramsky, Gay, Nagarajan
p.38 composition of two processes $p:A \rightarrow B$, $q:B \rightarrow C$ is defined as:
$ p;q = \{s\upharpoonright\Sigma_A,\Sigma_C \mid s \in Tr(\Sigma_A + \Sigma_B + \Sigma_C), s \upharpoonright \Sigma_A,\Sigma_B \in p, s \upharpoonright \Sigma_B,\Sigma_C \in q \} $
If I am reading it correctly, I would have rendered it as:
$ p;q = \{s\upharpoonright(\Sigma_A \cup \Sigma_C) \mid s \in Tr(\Sigma_A \cup \Sigma_B \cup \Sigma_C), s \upharpoonright (\Sigma_A \cup \Sigma_B) \in p, s \upharpoonright (\Sigma_B \cup \Sigma_C) \in q \} $
The LHS of the harpoon is a trace $s \in Tr(\Sigma)$ defined as a sequence of subsets of $\Sigma$. The RHS is a subset of an alphabet $X \subseteq \Sigma$. So far the rest of the paper has been clear on when notation is being 'abused' and nothing else has been questionable until this formula.
The main thing that's throwing me off is that alphabets are combined with '+' and ',' in different places (and so there are two "different" commas being used in the right hand side of the guard), but to me they look to be the same operation, namely set union. One possibility I've considered is that one of them is intended to be a disjoint union and the other an ordinary union.
Edit: It seems I missed the definition of '+' further up, so $Tr(\Sigma_A + \Sigma_B + \Sigma_C)$ is equivalent to $Tr(\Sigma_{A \otimes B \otimes C})$
$ p;q = \{s\upharpoonright(\Sigma_A \cup \Sigma_C) \mid s \in Tr(\Sigma_{A \otimes B \otimes C}), s \upharpoonright (\Sigma_A \cup \Sigma_B) \in p, s \upharpoonright (\Sigma_B \cup \Sigma_C) \in q \} $
