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.
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.
|Creators||Lenisa, M., Power, J. and Watanabe, H.|
|Departments||Faculty of Science > Computer Science|
Actions (login required)