Operational Semantics and Program Equivalence
Andy Pitts Computer Laboratory
Description
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/.