



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