Operational Semantics and Program Equivalence
Lectures by Andrew Pitts at
the International Summer School On Applied Semantics, APPSEM 2000,
Caminha, Minho, Portugal, 9-15 September 2000
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.
Some of the material in the following papers will be covered in