**Next:**Digital Communication II

**Up:**Michaelmas Term 2009: Part

**Previous:**Business Studies

**Contents**

##

Denotational Semantics

*Lecturer: Dr M.P. Fiore*

*No. of lectures:* 10 *(including revision)*

**Aims**

The aims of this course are to introduce domain theory and denotational semantics, and to show how they provide a mathematical basis for reasoning about the behaviour of programming languages.

**Lectures**

**Introduction.**The denotational approach to the semantics of programming languages. Recursively defined objects as limits of successive approximations.**Least fixed points.**-complete partial orders (cpos) and least elements. -continuous functions and least fixed points.**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.**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 with 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**

Books:

* Gunther, C. (1992). *Semantics of programming languages: Structures and techniques*. MIT Press.

Tennent, R. (1991). *Semantics of programming languages*. Prentice Hall.

* Winskel, G. (1993). *The formal semantics of programming languages: An introduction*. MIT Press.

Papers:

Fiore, M., Jung, A., Moggi, E., O'Hearn, P., Riecke, J., Rosolini, G. & Stark, I. (1996).
Domains and denotational semantics: History, accomplishments and
open problems.
*Bulletin of EATCS*, 59:227-256.

Ong, C.-H. (1995).
Correspondence between operational and denotational semantics.
*Handbook of Logic in Computer Science*, Vol. 4, pp. 269-356.

Plotkin, G. (1977).
LCF considered as a programming language.
*Theoretical Computer Science*, 5:223-256.

Scott, D. (1969).
A type-theoretical alternative to CUCH, ISWIM, OWHY.
In *Theoretical Computer Science*, 121:411-440, 1993.

**Next:**Digital Communication II

**Up:**Michaelmas Term 2009: Part

**Previous:**Business Studies

**Contents**