Title: Rule Formats for Nominal Process Calculi,
Abstract: The nominal transition systems (NTSs) of Parrow et al. describe the
operational semantics of nominal process calculi. We study NTSs in terms of the
nominal residual transition systems (NRTSs) that we introduce. We provide rule
formats for the specifications of NRTSs that ensure that the associated NRTS is
an NTS and apply them to the operational specifications of the early and late
pi-calculus. We also explore alternative specifications of the NTSs in which we
allow residuals of abstraction sort, and introduce translations between the
systems with and without residuals of abstraction sort. Our study stems from
the Nominal SOS of Cimini et al. and from earlier works in nominal sets and
nominal logic by Gabbay, Pitts and their collaborators.