Interleaving of atomic operations is used in the formal description of programming languages to represent both concurrency, and implementation-dependent aspects of a language.
Transitional Operational Semantics is well suited for the description of interleaving operations: however, proofs within this semantics setting can be large and cumbersome. On the other hand, proofs of properties in Relational Semantics setting can be simpler than in Transitional Semantics, but the description of interleaving constructors is problematic when side effects must be allowed to occur.
We look for a way of representing interleaving constructors in the elegant relational framework, while maintaining the simplicity of proofs. This is achieved by the addition of global information, to be known by all the branches of a relational proof-tree. An extended notation is given for rules and proof trees, and a principle of rule induction is provided.
A proof of the agreement between a transition semantics and an extended relational semantics for an imperative parallel language is sketched.