## Applications of Categories in Computer Science: Proceedings of the London Mathematical Society Symposium, Durham 1991M. P. Fourman, P. T. Johnstone, A. M. Pitts Category theory and related topics of mathematics have been increasingly applied to computer science in recent years. This book contains selected papers from the London Mathematical Society Symposium on the subject which was held at the University of Durham. Participants at the conference were leading computer scientists and mathematicians working in the area and this volume reflects the excitement and importance of the meeting. All the papers have been refereed and represent some of the most important and current ideas. Hence this book will be essential to mathematicians and computer scientists working in the applications of category theory. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Computational comonads and intensional semantics | 1 |

Weakly distributive categories | 45 |

Sequentiality and full abstraction | 66 |

Remarks on algebraically compact categories | 95 |

Dinaturality for free | 107 |

Simply typed and untyped lambda calculus revisited | 119 |

Modelling reduction in confluent categories | 143 |

On clubs and datatype constructors | 163 |

Strong monads algebras and fixed points | 202 |

Semantics of local variables | 217 |

Using fibrations to understand subtypes | 239 |

Reasoning about sequential functions via logical relations | 258 |

Icategories and duality | 270 |

Geometric theories and databases | 288 |

Partial products bagdomains and hyperlocal toposes | 315 |

Penrose diagrams and 2dimensional rewriting | 191 |

### Common terms and phrases

algebraic poset axioms bagdomain calculus cartesian closed category category theory classifying topos club colimits comonad composition computational comonad computational pairing Computer Science construction context coproducts corresponding Curien deﬁnable deﬁned deﬁnition denotational semantics denote diagram distributive categories domain elements endofunctor equations equivalence relation example exponentiation extensional ﬁbration ﬁbre ﬁnal ﬁnd ﬁnite products ﬁrst ﬁxed point object ﬂat full abstraction full subcategory fully abstract geometric morphism given hence I-category identiﬁed identity inclusion indexed category inﬁnite initial algebra intensional isomorphism Kleisli category lambda calculus left adjoint Lemma merge monoidal structure natural numbers natural transformations notion observe obtain Plotkin pointwise polycategory poset powerdomain preserves Proof Proposition pullback reduction reﬂective result satisﬁes semantics sequence sequential algorithms speciﬁcation split strict strong dinatural strong monad subcategory subset subtyping T-algebra tensor Theorem Top/S toposes types unique variables weakly distributive category