Domains and Lambda-Calculi

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