Department of Computer Science and Technology

Part II CST

Denotational Semantics

Principal lecturer: Prof Marcelo Fiore
Taken by: Part II CST
Term: Michaelmas
Hours: 10
Format: In-person lectures
Suggested hours of supervisions: 2
Exam: Paper 8 Question 4, 4; Paper 9 Question 5, 5
Past exam questions, Moodle, timetable

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.Flat domains.Product domains. Function 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. [2 lectures].
• 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. [2 lectures].
• Full abstraction.Failure of full abstraction for the domain model. PCF with parallel or.

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.