by Thomas Streicher (Technical University Darmstadt, Germany)

Table of Contents (133k)
Preface (114k)
Chapter 1: Introduction (227k)

This textbook provides a basis for a PhD course on domain-theoretic semantics of functional programming languages and their meta-mathematical properties. It introduces basic domain theory and the technique of logical relations as developed by Scott and Plotkin. The solution of recursive domain equations is explained in detail.

A complete discussion of the famous full abstraction problem for PCF (a functional Kernel language due to Scott and Plotkin) is given including a construction of the fully abstract Milner model using Kripke logical relations.

A final chapter introduces computability in Scott domains and shows that this model is fully abstract and universal for appropriate extensions of PCF by parallel language constructs.

• PCF and Its Operational Semantics
• The Scott Model of PCF
• Computational Adequacy
• Milner's Context Lemma
• The Full Abstraction Problem
• Logical Relations
• Some Structural Properties of the Dσ
• Solutions of Recursive Domain Equations
• Characterisation of Fully Abstract Models
• Sequential Domains as a Model of PCF
• The Model of PCF in S is Fully Abstract
• Computability in Domains