



Next: Digital Communication II Up: Michaelmas Term 2007: Part Previous: Business Studies Contents
Denotational Semantics
Lecturer: Professor G. Winskel
No. of lectures: 8
Prerequisite course: Semantics of Programming Languages (specifically, an idea of operational semantics and how to reason from it)
Aims
The aims of this course are to introduce domain theory and denotational semantics, and show how they can provide a mathematical basis for reasoning about the behaviour of programming languages.
Lectures
- Introduction.
Recursively defined objects as limits of successive approximations.
Examples.
- Least fixed points.
-complete partial orders (cpos) and
-continuous functions. Least elements. Least fixed points of
-continuous functions.
- Constructions on domains.
Products of domains. Function domains. Flat domains.
- Scott induction.
Chain-closed and admissible subsets of cpos and domains. Scott's
fixed point induction principle. Examples.
- PCF.
The Scott-Plotkin language PCF. Evaluation. Contextual equivalence.
- Denotational semantics of PCF.
Denotation of types and terms. Compositionality. Soundness with
respect to evaluation.
- Relating denotational and operational semantics.
Formal approximation relation and its fundamental property.
Computational adequacy of the PCF denotational semantics with
respect to evaluation. Extensionality properties of contextual
equivalence.
- Full abstraction.
Failure of full abstraction for the domain model. PCF plus parallel
or. Recent developments.
Objectives
At the end of the course students should:
- be familiar with basic domain theory, cpos, continuous
functions, admissible subsets, least fixed points, basic constructions
on domains
- be able to give denotational semantics to simple programming
languages with simple types
- be able to apply denotational semantics, in particular, to
understand the use of least fixed points to model recursive programs
and be able to reason about least fixed points and simple recursive
programs using fixed point induction
- understand the issues concerning the relation between
denotational and operational semantics, adequacy and full abstraction,
especially with respect to the language PCF
Recommended reading
* Winskel, G. (1993). The formal semantics of programming languages. MIT Press.
Tennent, R.D. (1991). Semantics of programming languages. Prentice-Hall.




Next: Digital Communication II Up: Michaelmas Term 2007: Part Previous: Business Studies Contents