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.
Author(s): Thomas Streicher
Publisher: World Scientific Publishing Company
Year: 2006
Language: English
Pages: 120
Contents ......Page 8
Preface ......Page 10
1. Introduction ......Page 12
2. PCF and its Operational Semantics ......Page 24
3. The Scott Model of PCF ......Page 34
3.1 Basic Domain Theory ......Page 36
3.2 Domain Model of PCF ......Page 43
3.3 LCF - A Logic of Computable Functionals ......Page 45
4. Computational Adequacy ......Page 48
5. Milner's Context Lemma ......Page 54
6. The Full Abstraction Problem ......Page 56
7. Logical Relations ......Page 62
8. Some Structural Properties of the Dσ......Page 68
9. Solutions of Recursive Domain Equations ......Page 76
10. Characterisation of Fully Abstract Models ......Page 88
11. Sequential Domains as a Model of PCF ......Page 98
12. The Model of PCF in S is Fully Abstract ......Page 106
13. Computability in Domains ......Page 110
Bibliography ......Page 128
Index ......Page 130
