Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Andrew Pitts
Operational Semantics and Program Equivalence
Computer Laboratory > Andrew Pitts > Recent Talks > Operational Semantics and Program Equivalence

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


  • Revised version of the lecture notes [pdf] (Original version here [pdf].)

  • Abstract

    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.

    Prerequisites

  • Some familiarity with the basic ideas of structural operational semantics, for example as presented in the first 5 sections of Semantics of Programming Languages, lectures by Andrew Pitts for the Cambridge University Computer Science Tripos, Part IB.
  • Some familiarity with a programming language in the ML family, such as OCaml or SML.
  • Further reading

    Some of the material in the following papers will be covered in the lectures:
  • A.M. Pitts and I.D.B. Stark, Operational Reasoning for Functions with Local State. In A.D. Gordon and A.M. Pitts (Eds), Higher Order Operational Techniques in Semantics, Publications of the Newton Institute (Cambridge University Press, 1998), pp 227-273.
  • A.M. Pitts, Parametric Polymorphism and Operational Equivalence, Mathematical Structures in Computer Science 10(2000) 1-39.