Michael Johnson
(mike@mpce.mq.edu.au)
School of Maths and Computing
Macquarie University
Sydney, 2109, Australia.
Tel: +61 2 850 9583
Fax: +61 2 850 9551
Computational category theory is particularly interesting because not only is category theory a branch of algebra (and so computational algebra techniques that have already been developed are frequently valuable in category theory) but also algebra is a branch of category theory (and so category theoretic techniques and application domains are likely to be relevant for computational algebra). (The view of algebra as a branch of category theory is made precise in categorical universal algebra.)
Despite these close connections, there has not before now been a significant conference opportunity for category theorists and workers in the rest of computational algebra to interact. We hope that this session and this conference will provide that long missing opportunity.
The talks for this session have been chosen to be representative of the major threads mentioned above. Here are three examples (there are actually seven talks and their abstracts are below).
Richard Buckland will describe a concrete application of computational category theory in which a system designed to perform computations in n-categories is used as the engine for a computer assisted software engineering (CASE) tool for concurrent systems.
Robert Walters and his colleagues have developed arguably the most significant new procedure in computational category theory. This procedure is a very good example of the interaction of computer algebra and computational category theory: it is based on the famous Todd-Coxeter procedure which has been widely used in computer algebra, but it requires significant generalisation beyond the normal Todd-Coxeter, and it has in turn led to a new and simple proof of the correctness of the Todd-Coxeter procedure, even in its classical use for enumerating cosets.
Ronnie Brown has been working with colleagues including Winfried Dreckmann on developing an integrated system for computational category theory. The preceding two talks have shown some of the progress being made in computational category theory, but without an integrated system each new algorithm usually uses new and incompatible data types and the systems remain special purpose and generally hard to use. Of course systems for computational category theory should take advantage of the developed systems for computational algebra, and Brown and Dreckmann have been investigating the use of the Axiom computational algebra system for supporting computational category theory.
