Semantics of Programming Languages

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

No. of lectures: 12  

Introduction.

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

Induction.

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

Structural operational semantics.

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

Functions.

Binding constructs, substitution and -conversion. Call-by-name and call-by-value function application. Static semantics of simply typed languages and its relation to evaluation.

Locality.

Local recursive definitions. Block-structured local state. Dynamically allocated local state.

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.

Interaction.

Labelled transition systems. A simple imperative language with interactive input/output. Interaction by synchronised communication on channels.

Co-induction.

Inductively defined sets as least pre-fixed points of monotone functions, including proof of existence and fixed point property. Co-inductively defined sets as greatest post-fixed points. Examples.

Recommended books:

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

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