Semantics of Programming Languages

Lecturer: Dr A.M. Pitts (ap@cl.cam.ac.uk)

No. of lectures: 12

This course is a prerequisite for Denotational Semantics (Part II) and Types (Part II). It is also useful for Communicating Automata and Pi Calculus (Part II).

This course provides an introduction to the structural, operational approach to programming language semantics.

Introduction.

Transition systems. Example: an abstract machine for a simple imperative language. The idea of structural operational semantics. [1 lecture]

Induction.

Review of mathematical induction. Abstract syntax trees and structural induction. Rule-based inductive definitions and proofs. [1 lecture]

Structural operational semantics.

Inductively defined transition and evaluation relations for a simple imperative language and the relationship between them. [2 lectures]

Functions.

Binding constructs, substitution and $\alpha$-conversion. Call-by-name and call-by-value function application. Static semantics of simply typed languages and its relation to evaluation. [2 lectures]

Locality.

Local recursive definitions. Block-structured local state. Dynamically allocated local state. [2 lectures]

Semantic equivalence.

Semantic equivalence of phrases in a simple imperative language, including the congruence property. Examples of equivalence and non-equivalence. The notion of contextual equivalence of program phrases. [2 lectures]

Interaction.

Labelled transition systems. A simple imperative language with interactive input/output. Interaction by synchronised communication on channels. Co-inductively defined notions of semantic equivalence. [2 lectures]

Recommended books:

Hennessy, M. (1990). The Semantics of Programming Languages. Wiley.

Winskel, G. (1993). The Formal Semantics of Programming Languages. MIT Press.