This book describes the mathematical aspects of the semantics of programming languages. The main goals are to provide formal tools to assess the meaning of programming constructs in both a language-independent and a machine-independent way and to prove properties about programs, such as whether they terminate, or whether their result is a solution of the problem they are supposed to solve. In order to achieve this the authors first present, in an elementary and unified way, the theory of certain topological spaces that have proved of use in the modeling of various families of typed lambda calculi considered as core programming languages and as meta-languages for denotational semantics. This theory is now known as Domain Theory, and was founded as a subject by Scott and Plotkin. One of the main concerns is to establish links between mathematical structures and more syntactic approaches to semantics, often referred to as operational semantics, which is also described. This dual approach has the double advantage of motivating computer scientists to do some mathematics and of interesting mathematicians in unfamiliar application areas from computer science.
Author(s): Roberto M. Amadio, Pierre-Louis Curien
Series: Cambridge Tracts in Theoretical Computer Science 46
Publisher: Cambridge University Press
Year: 1998
Language: English
Pages: 536
Contents......Page 3
Preface......Page 7
Notation......Page 13
1. Continuity and Computability......Page 15
1. Directed completeness and algebraicity......Page 16
2. Dcpo's as topological spaces......Page 22
3. Computability and continuity......Page 24
4. Constructions and dcpo's......Page 25
5. Toy denotational semantics......Page 31
6. Continuation semantics......Page 34
2. Syntactic Theory of the λ-calculus......Page 37
1. Untyped λ-calculus......Page 38
2. The labelled λ-calculus......Page 45
3. Syntactic continuity......Page 53
4. The syntactic sequentiality theorem......Page 56
1. D_∞ models......Page 59
2. Properties of D_∞ models......Page 64
3. Filter models......Page 70
4. Some D_∞ models as filter models......Page 77
5. More on intersection types......Page 81
4. Interpretation of λ-Calculi in CCC's......Page 89
1. Simply typed λ-calculus......Page 90
2. Cartesian closed categories......Page 94
3. Interpretation of λ-calculi......Page 98
4. From CCC's to λ-theories and back......Page 101
5. Logical relations......Page 104
6. Interpretation of the untyped λ-calculus......Page 119
1. Continuous dcpo's......Page 125
2. Bifinite domains and L-domains......Page 128
3. Full sub-CCC's of acpo......Page 136
4. Full sub-CCC's of adcpo......Page 141
5. Completeness of well-ordered lub's......Page 143
1. The λY-calculus......Page 147
2. Fixpoint induction......Page 149
3. The programming language PCF......Page 151
4. The full abstraction problem for PCF......Page 155
5. Towards sequentiality......Page 165
1. Domain equations......Page 169
2. Predicate equations......Page 180
3. Universal domains......Page 183
4. Representation......Page 188
8. Values and Computations......Page 193
1. Representing computations as monads......Page 194
2. Call-by-value and partial morphisms......Page 201
3. Environment machines......Page 207
4. A FA model for a parallel λ-calculus......Page 211
5. Control operators and CPS translation......Page 217
1. Monads of powerdomains......Page 227
2. CCS......Page 231
3. Interpretation of CCS......Page 236
1. Topological spaces and locales......Page 243
2. The duality for algebraic dcpo's......Page 251
3. Stone spaces......Page 255
4. Stone duality for bifinite domains......Page 258
5. Scott domains in logical forms......Page 260
6. Bifinite domains in logical form......Page 267
11. Dependent and Second Order Types......Page 269
1. Domain-theoretical constructions......Page 271
2. Dependent and second order types......Page 280
3. Types as retractions......Page 284
4. System LF......Page 288
5. System F......Page 293
12. Stability......Page 301
1. Conditionally multiplicative functions......Page 302
2. Stable functions......Page 307
3. dI-domains and event structures......Page 313
4. Stable bifinite domains......Page 320
5. Connected glb's......Page 328
6. Continuous L-domains......Page 333
13. Towards linear logic......Page 337
1. Coherence spaces......Page 338
2. Categorical interpretation of linear logic......Page 342
3. Hypercoherences and strong stability......Page 353
4. Bistructures......Page 362
5. Chu spaces and continuity......Page 373
14. Sequentiality......Page 381
1. Sequential functions......Page 382
2. Sequential algorithms......Page 387
3. Algorithms as strategies......Page 398
4. Full abstraction for PCF + catch......Page 419
15. Domains and realizability......Page 431
1. A universe of realizable sets......Page 434
2. Interpretation of system F......Page 437
3. Interpretation of type assignment......Page 439
4. Partiality and separation in per......Page 444
5. Complete per's......Page 448
6. Per's over D_∞......Page 456
7. Interpretation of subtyping......Page 462
1. π-calculus......Page 467
2. A concurrent functional language......Page 482
1. Partial recursive functions......Page 497
2. Recursively enumerable sets......Page 499
3. Rice-Shapiro theorem......Page 501
Appendix B. Memento of Category Theory......Page 503
1. Basic definitions......Page 504
2. Limits......Page 505
3. Functors and natural transformations......Page 508
4. Universal morphisms and adjunctions......Page 510
5. Adjoints and limits......Page 513
6. Equivalences and reflections......Page 514
7. Cartesian closed categories......Page 516
8. Monads......Page 517
Bibliography......Page 519
List of figures......Page 529
Index......Page 532
