Towards a Mathematical Operational Semantics

Daniele Turi and Gordon Plotkin

In Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS '97, pages 280--291. IEEE Computer Society Press, 1997.

Available as PostScript (262K).


We describe operational rules abstractly as natural transformations of a type depending on functorial notions of syntax and behaviour. Every such natural transformation induces a distributive law between the syntax and the behaviour. The bialgebras of this distributive law are combinations of denotational and operational models which are always `adequate' with respect to the original rules. In particular, the final bialgebra is fully-abstract with respect to the equivalence on operational models corresponding to the behaviour. The theory specialises to the known classes of well-behaved rules for structural operational semantics.

  Author={Turi, D. and Plotkin, G.D.},
  Title={Towards a mathematical operational semantics},
  Publisher={Computer Society Press},
  Booktitle={Proc.\ 12$^{\rm th}$ LICS Conf.},
  source = {}

Daniele Turi
Last modified: Mon Jun 12 13:49:09 BST 2000