Category theory for operational semantics

We use the concept of a distributive law of a monad over a copointed endofunctor to define and develop a reformulation and mild generalisation of Turi and Plotkin's notion of an abstract previous termoperationalnext term rule. We make our abstract definition and give a precise analysis of the relationship between it and Turi and Plotkin's definition. Following Turi and Plotkin, our definition, suitably restricted, agrees with the notion of a set of GSOS-rules, allowing one to construct both an previous termoperationalnext term model and a canonical, internally fully abstract denotational model. Going beyond Turi and Plotkin, we construct what might be seen as large-step previous termoperationalnext term semantics from small-step previous termoperationalnext term semantics and we show how our definition allows one to combine distributive laws, in particular accounting for the combination of previous termoperationalnext term semantics with congruences.