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

*No. of lectures:* 12

*This course is a prerequisite for Types *(*Part II*)* and
Topics in Concurrency *(*Part II*)*.*

**Aims**

The aim of this course will be to introduce the structural, operational approach to programming language semantics. It will show how this formalism is used to specify the meaning of some simple programming language constructs and to reason formally about semantic properties of programs.

**Lectures**

**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]**Semantic equivalence.**Semantic equivalence of phrases in a simple imperative language, including the congruence property. Examples of equivalence and non-equivalence. [2 lectures]**Functions.**Binding constructs, substitution and -conversion. Call-by-name and call-by-value function application. Local recursive definitions. Static semantics of simply typed languages and its relation to evaluation. The notion of contextual equivalence of program phrases. [3 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. [3 lectures]

**Objectives**

At the end of the course students should

- be familiar with rule-based presentations of the operational
semantics of 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
rule-based)
- 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.

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