Category theory for operational semantics

Marina Lenisa, John Power, Hiroshi Watanabe

Research output: Contribution to journalArticle

34 Citations (Scopus)

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 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
Volume327
Issue number1-2
DOIs
Publication statusPublished - 25 Oct 2004

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

Cite this