Operational Semantics and Program Equivalence

Andy Pitts

Computer Laboratory


The various approaches to giving meanings to programming languages fall broadly into three categories: denotational, axiomatic and operational. In a denotational semantics the meaning of programs is defined abstractly using elements of some suitable mathematical structure; in an axiomatic semantics, meaning is defined via some logic of program properties; and in an operational semantics it is defined by specifying the behaviour of programs during execution. Operational semantics used to be regarded as less useful than the other two approaches for many purposes, because it tends to be quite concrete, with important general properties of a programming language obscured by a low-level description of how program execution takes place. The situation changed with the development of a structural approach to operational semantics initiated by Plotkin, Milner, Kahn, and others. Structural operational semantics is now widely used for specifying and reasoning about the semantics of programming languages. In this course I attempt a brief tour of the different approaches to structural operational semantics, concentrating on the advantages and disadvantages of each for reasoning about operational equivalence of programs. I will argue that one particular and possibly unfamiliar approach using a `frame stack' formalism---derived from the approach of Wright and Felleisen and used in the recent redefinition of ML by Harper and Stone---provides a more convenient basis for developing properties of contextual equivalence of programs than does the evaluation (or `natural', or `big-step') semantics used in the official definition of Standard ML by Milner et al.

A web page for this course from where the notes can be downloaded is at http://www.cl.cam.ac.uk/users/amp12/papers/opespe/.