A congruence rule format for name-passing process calculi

We introduce a GSOS-like rule format for name-passing process calculi. Specifications in this format correspond to theories in nominal logic. The intended models of such specifications arise by initiality from a general categorical model theory. For operational semantics given in this rule format, a natural behavioural equivalence—a form of open bisimilarity—is a congruence.