![[Search]](http://www.cl.cam.ac.uk/images/search.gif){kind=small}
![[A-Z Index]](http://www.cl.cam.ac.uk/images/az.gif){kind=small}
![[Contact]](http://www.cl.cam.ac.uk/images/contact.gif){kind=small}
![[University of Cambridge]](http://www.cl.cam.ac.uk/images/identifier2.gif){kind=small}
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