Next: Concurrent Systems
Up: Michaelmas Term 1999: Part
Previous: ECAD
Lecturer: Dr A.M. Pitts (ap@cl.cam.ac.uk)
No. of lectures: 12
This course is a prerequisite for Types (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
Recommended books
Hennessy, M. (1990). The Semantics of Programming Languages.
Wiley.
Winskel, G. (1993). The Formal Semantics of Programming
Languages. MIT Press.
Next: Concurrent Systems
Up: Michaelmas Term 1999: Part
Previous: ECAD
Christine Northeast
Mon Sep 20 10:28:43 BST 1999