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).

Abstract

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.

@InProceedings{TP97,
  Author={Turi, D. and Plotkin, G.D.},
  Title={Towards a mathematical operational semantics},
  Organization={IEEE},
  Publisher={Computer Society Press},
  Booktitle={Proc.\ 12$^{\rm th}$ LICS Conf.},
  Pages={280-291},
  Year=1997,
  source = {http://www.dcs.ed.ac.uk/home/dt/}
}