A non-interleaving semantics for CCS based on proved transitions, with I. Castellani, in Fundamentae Informaticae XI (1988), 433-453.

When using labelled transition systems to model languages like CCS or TCSP, one specifies transitions by a set of structural rules. We consider labelling transitions with their proofs - in the given system of rules - instead of simple actions. Then the label of a transition identifies uniquely that transition, and one may use this information to define a concurrency relation on (proved) transitions, and a notion of residual of a (proved) transition by a concurrent one. We apply Berry and Lévy's notion of equivalence by permutations to sequences of transitions for CCS to obtain a partial order semantics for this language.