Category theory for operational semantics

Marina Lenisa, John Power, Hiroshi Watanabe

Research output: Contribution to journalArticlepeer-review

35 Citations (SciVal)


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.
Original languageEnglish
Pages (from-to)135-154
Number of pages20
JournalTheoretical Computer Science
Issue number1-2
Publication statusPublished - 25 Oct 2004


Dive into the research topics of 'Category theory for operational semantics'. Together they form a unique fingerprint.

Cite this