Applications of Categories in Computer Science: Proc. London Math. Soc. Symp., Durham 1991

Title Page ......Page 3
Contents ......Page 5
Preface ......Page 7
Computational Comonads and Intensional Semantics ......Page 11
1 Introduction ......Page 12
2.1 Comonads and the Kleisli category ......Page 14
3 Notions of computation on domains ......Page 16
3.1 Increasing paths ......Page 17
3.2 Strictly increasing paths ......Page 22
3.3 Timed data ......Page 23
4.1 Computational comonads ......Page 25
4.2 Examples ......Page 30
5.1 Products ......Page 33
5.2 Exponentiation ......Page 35
5.3 Examples ......Page 38
5.4 Pairing, currying and uncurrying on algorithms ......Page 39
5.5 Examples ......Page 43
6 Ordered categories ......Page 44
7.2 Strict algorithms ......Page 48
7.3 Computation on effectively given domains ......Page 49
7.4 Computation on pre-domains ......Page 50
8 Conclusions ......Page 51
References ......Page 53
0. Introduction ......Page 55
1. Polycategories ......Page 57
2.1. Definition ......Page 62
2.2. Weakly distributive categories and polycategories ......Page 64
3. Distributive categories ......Page 65
4. Adding negation ......Page 69
5. Some posetal examples ......Page 73
References ......Page 75
1 Introduction ......Page 76
2 Syntactic sequentiality ......Page 77
3 Full abstraction for PCF and related languages ......Page 83
4 Sequential algorithms on concrete data structures ......Page 93
5 One, two, hundred errors ......Page 98
References ......Page 102
Remarks on Algebraically Compact Categories ......Page 105
1: On some examples ......Page 106
2: On CPO-categories ......Page 107
4: On the Product Theorems ......Page 110
5: On Dinaturality ......Page 113
6: On Multi-Coreflectivity ......Page 114
7: On Relation Categories ......Page 115
Dinaturality for free ......Page 117
1. The problem ......Page 118
2. Some properties of an internal functor ......Page 119
3. When the hexagon commutes ......Page 122
4. The algebraic case ......Page 124
References ......Page 127
1. Introduction ......Page 129
2. Preliminaries ......Page 131
3. Simply typed λ-calculus ......Page 134
4. The untyped λ-calculus ......Page 143
References ......Page 151
1. Introduction ......Page 153
2. Confluent Categories ......Page 156
3. Confluent Adjunctions ......Page 159
4.2. Contexts and Declarations ......Page 162
5.1. The Reduction System ......Page 166
5.2. A Substitution Model ......Page 168
5.3. A Declaration Model ......Page 169
6. Further Work ......Page 170
References ......Page 171
1. Introduction ......Page 173
2. The original club idea ......Page 174
3. The abstract notion of club ......Page 180
4. The enriched case ......Page 186
5. The original clubs are clubs in the abstract sense; other examples and counter-examples ......Page 192
References ......Page 198
1. A finite presentation ......Page 201
2. A complete rewrite system ......Page 203
3. Carrying on ......Page 204
References ......Page 205
Appendix: Confluence of the fifty-six critical pairs ......Page 209
1. Introduction ......Page 212
2. Strong dinaturality and fix ......Page 213
3. Algebraically strong dinaturality and FIX ......Page 218
References ......Page 226
1 Introduction ......Page 227
2 Possible Worlds ......Page 228
3 Procedures ......Page 233
4 States and Contravariance ......Page 235
5 Generalized Variables ......Page 237
6 Non-interference ......Page 240
7 Discussion ......Page 245
Acknowledgements ......Page 246
References ......Page 247
1.1. What this paper is about ......Page 249
1.2. Fibrations and polymorphic λ-calculus ......Page 252
2.1. Rules for subtypes and bounded quantification ......Page 254
2.2. Characterising inclusions ......Page 256
2.3. Incorporating bounded quantification ......Page 258
2.4. Incorporating subkinds ......Page 259
3.1. PER models ......Page 261
3.2. Models arising from PER models ......Page 263
3.3. Subtypes and constructions on types ......Page 264
References ......Page 265
2. Sequential PCF ......Page 268
3. Logical Relations ......Page 271
4. A Full Abstraction Result ......Page 275
5. Conclusion ......Page 278
References ......Page 279
Introduction ......Page 280
1. I-categories ......Page 281
2.1. Colimit/limit coincidence. Dual I-categories. ......Page 288
2.2. Initial/final algebras. ......Page 289
2.3. Conservative extensions. ......Page 290
3. Induction and Coinduction ......Page 292
References ......Page 295
Geometric Theories and Databases ......Page 298
1. Introduction ......Page 299
2. Geometric logic ......Page 303
2.1 Flat functors and Diaconescu's Theorem ......Page 307
2.2 Geometric logic as observational logic ......Page 309
3. The lower bagdomain ......Page 312
4. The mixed bagdomain ......Page 317
5.2 Continuous domains ......Page 321
5.5 Dynamic predicate geometric logic ......Page 322
References ......Page 323
1. Introduction ......Page 325
2. Indexed Coproducts ......Page 327
3. Partial Products ......Page 330
4. Algebraic Bagdomains ......Page 335
5. The Bagdomain Monad and its Algebras ......Page 338
6. Bagdomains and Scones ......Page 342
7. Bagdomains and Powerdomains ......Page 345
8. Upper and Mixed Bagdomains ......Page 346
References ......Page 348