Denotational Semantics

Lecturer: Dr A.M. Pitts (ap@cl.cam.ac.uk)

No. of lectures: 8

Prerequisite course: Semantics of Programming Languages

Introduction.

Recursively defined objects as limits of successive approximations. Examples.

Least fixed points.

omega-complete partial orders (cpos) and omega-continuous functions. Least elements. Tarski's fixed point theorem.

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. Examples.

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 plus parallel or. Recent developments.

Recommended books:

Winskel, G. (1993). The Formal Semantics of Programming Languages. MIT Press.

Tennent, R.D. (1991). Semantics of Programming Languages. Prentice-Hall.