Category theory for operational semantics


Lenisa, M., Power, J. and Watanabe, H., 2004. Category theory for operational semantics. Theoretical Computer Science, 327 (1-2), pp. 135-154.

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Official URL:


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.


Item Type Articles
CreatorsLenisa, M., Power, J. and Watanabe, H.
DepartmentsFaculty of Science > Computer Science
ID Code5466


Actions (login required)

View Item