



Next: Digital Communication II Up: Michaelmas Term 2008: Part Previous: Computer Systems Modelling Contents
Denotational Semantics
Lecturer: Dr M.P. Fiore
No. of lectures: 10 (including revision)
Prerequisite course: Semantics of Programming Languages (specifically, an idea of operational semantics and how to reason with it).
Aims
The aims of this course are to introduce domain theory and denotational semantics, and 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.,
and Stark, I. (1996).
Domains and denotational semantics: History, accomplishments and
open problems.
Bulletin of EATCS, 59:227-256.
Milner, R. (1977).
Fully abstract models of typed lambda-calculi.
Theoretical Computer Science, 4:1-22.
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 2008: Part Previous: Computer Systems Modelling Contents