Towards a Mathematical Operational Semantics
View/ Open
Date
05/11/2003Author
Plotkin, Gordon
Turi, Daniele
Metadata
Abstract
We present a categorical theory of ‘well-behaved’
operational semantics which aims at complementing
the established theory of domains and denotational semantics to form a coherent whole. It is shown that, if
the operational rules of a programming language can be
modelled as a natural transformation of a suitable general form, depending on functorial notions of syntax
and behaviour, then one gets the following for free: an
operational model satisfying the rules and a canonical,
internally fully abstract denotational model which satisfies the operational rules. The theory is based on distributive laws and bialgebras; it specialises to the known
classes of well-behaved rules for structural operational
semantics, such as GSOS.