This course is a prerequisite for Types (Part II), Denotational Semantics (Part II), and Topics in Concurrency (Part II).
The aim of this course is to introduce the structural, operational
approach to programming language semantics. It will show how to
specify the meaning of typical programming language constructs, in the
context of language design, and how to reason formally about semantic
properties of programs.
Introduction. Transition systems.
The idea of structural operational semantics.
Transition semantics of a simple imperative language.
Language design options.
Types. Introduction to formal type systems.
Typing for the simple imperative language.
Statements of desirable properties.
Induction. Review of mathematical induction. Abstract
syntax trees and structural induction. Rule-based inductive
definitions and proofs. Proofs of type safety
properties. [2 lectures]
Functions. Call-by-name and call-by-value function
application, semantics and typing. Local recursive
definitions. [2 lectures]
Data. Semantics and typing for products, sums, records,
Semantic equivalence. Semantic equivalence of phrases in a
simple imperative language, including the congruence property.
Examples of equivalence and non-equivalence.
Concurrency. Shared variable interleaving. Semantics for
simple mutexes; a serializability property.
Subtyping. Record subtyping and simple object
be familiar with rule-based presentations of the operational
semantics and type systems for some simple imperative, functional
and interactive program constructs
be able to prove properties of an operational semantics using
various forms of induction (mathematical, structural, and
be familiar with some operationally-based notions of semantic
equivalence of program phrases and their basic properties
Hennessy, M. (1990). The semantics of programming languages. Wiley. Out of print, but available on the web at http://www.cogs.susx.ac.uk/users/matthewh/semnotes.ps.gz * Pierce, B.C. (2002). Types and programming languages. MIT Press.
Winskel, G. (1993). The formal semantics of programming languages. MIT Press.