Seminars of the CENTRE de RECHERCHE en THEORIE des CATEGORIES CATEGORY THEORY RESEARCH CENTER C ---------> R | / | | / | | / | | / | v / v T ---------> C PLACE: BURNSIDE HALL 920, McGILL UNIVERSITY (COFFEE AND COOKIES AS USUAL AT 3:30 IN THE LOUNGE) Tuesday, 10 September 1991 2:00-3:30 M. Makkai (McGill University) "Craig Interpolation" 4:00-5:30 J. Lambek "Bilinear logic" Tuesday, 17 September 1991 2:00-3:30 Gonzalo E. Reyes (Universite de Montreal) "Bi-Heyting Algebras" 4:00-5:30 Prakash Panangaden (McGill University) "Constraint programming and a realizability interpretation of linear logic" Tuesday, 24 September 1991 2:00-3:30 R. Seely (McGill) "Weakly distributive categories" 4:00-5:30 M. Barr (McGill) "Fuzzy models of linear logic" Tuesday, 1 October 1991 2:00-3:30 Luc Belair (UQAM) "Infinitesimally stable theories of Henselian rings" 4:00-5:30 Jonathan Funk (McGill) "The cocontinuous dual of a topos" Tuesday, 8 October 1991 2:00-3:30 J. Lambek (McGill) "On a completion of categories" 4:00-5:30 M. Barr (McGill) "Terminal coalgebras" Tuesday, 15 October 1991 2:00-3:30 S. Brookes (CMU) "A Cartesian Closed Category of Parallel Algorithms between Scott Domains" (abstract below) 4:00-5:30 M. Okada (Concordia) "A proof theoretic analysis on some categorical uniqueness conditions of typed functional languages" Tuesday, 22 October 1991 2:00-3:30 W. Brierley (McGill) "Types in the general scheme of things - a general spectrum construction" 4:00-5:30 R. Blute (McGill) "Proof nets and coherence theorems" Tuesday, 29 October 1991 2:00-3:30 H. Hu "On cone-injectivity in locally presentable categories" Tuesday, 5 November 1991 2:00-3:30 J. Rosicky (York) "Accessible categories and model theory" Tuesday, 12 November 1991 2:00-3:30 M. Barr (McGill) "Algebraically compact categories and functors" 4:00-5:30 T. Fox (McGill) "Cofree coalgebras and the cohomology of bialgebras" Tuesday, 19 November 1991 2:00-3:30 A. Urquhart (Toronto) "Lower bound on complexity of relevant implication" 4:00-5:30 J. Otto (McGill) "A categorical characterisation of polynomial-time functions" Tuesday, 26 November 1991 2:00-3:30 R.A.G. Seely (McGill) "(2-sided) Proof nets for weakly distributive categories" 4:00-5:30 R. Blute (McGill) "Dinaturality and polymorphism" Tuesday, 3 December 1991 2:00-5:30 M. Makkai (McGill) and G.E. Reyes (U. Montreal) "Completeness and interpolation for biheyting and bimodal logics, I and II" == ABSTRACTS: ============================================================= Stephen Brookes Carnegie Mellon University School of Computer Science ABSTRACT We present a category-theoretic framework for providing intensional semantics for programming languages and establishing connections between semantics given at different levels of abstraction. The key idea is to model an abstract notion of computation as a comonad, and to use the Kleisli construction to build a category whose morphisms (or ``algorithms'') map computations to results. This allows distinctions and comparisons to be made between different programs computing the same function, on the basis of their computation strategy. We illustrate by developing a category of parallel algorithms between Scott domains, obtained from the category of Scott domains and continuous functions with a notion of computation as increasing sequence of values. Every algorithm computes a continuous function from values to values, and every such function is computed by some algorithm. The algorithm category is cartesian closed, so that currying and uncurrying are natural isomorphisms and application morphisms exist with the usual properties. In addition the algorithms category permits non-standard forms of currying, uncurrying and application that satisfy weaker versions of these properties. This means that, for instance, one may use the intensional category to interpret a functional programming language containing more than one form of application, currying and uncurrying, as may be desirable if we want to maintain a distinction between strict and non-strict, call-by-value and call-by-name, or sequential and parallel. We discuss the generality of our approach, its applicability in other settings, and the relationship with earlier work. We can define a category of dI-domains and stable algorithms, in which every algorithm computes a stable function. The Berry-Curien category of sequential algorithms between concrete domains can be embedded in our category in a natural way that respects the operational behavior of algorithms. This is joint work with Shai Geva.