Forms of Semantic Specification

Machine M 0 \Gamma!M 1 \Gamma!M 2 \Gamma!M 3 \Gamma! \Delta \Delta \Delta \Gamma!M n Transition Semantics M + V Natural Semantics Figure 1: Three forms of operational semantics. Flemming Nielson [NN91]; similar languages are examined in [Ten91]. My own book [Gun92] focuses on the language PCF and its extensions. There is a growing literature on the relationships between various forms of operational semantics. Research of John Hannan [Han91, HM92] has helped to clarify some of the distinctions between these different forms of operational semantics and I refer the reader to his work for a further treatment. There is also an approach to operational semantics that focuses on evaluation contexts; it has been used to study the relationships between different forms of semantic specification in languages that include control constructs [FFKD87] and the approach seems to work well for proofs that type systems exclude certain kinds of errors [WF91]. Before closing, let me make a comment on a me..