- Abstract:
-
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 operational 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 operational model and a canonical, internally fully abstract denotational model. Going beyond Turi and Plotkin, we construct what might be seen as large-step operational semantics from small-step operational semantics and we show how our definition allows one to combine distributive laws, in particular accounting for the combination of operational semantics with congruences.
- Copyright:
- 2004 Elsevier B.V. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @Article{EDI-INF-RR-0412,
- author = {
Marina Lenisa
and John Power
and Hiroshi Watanabe
},
- title = {Category theory for operational semantics},
- journal = {Theoretical Computer Science},
- publisher = {Elsevier},
- year = 2004,
- volume = {327},
- pages = {135-154},
- doi = {10.1016/j.tcs.2004.07.024},
- }
|
