%==============
\begin{center}
{\LARGE \bf Computational Category Theory
}
\end{center}
%==============
\bigskip

{\bf Organizer}

\medskip

Michael Johnson (mike@mpce.mq.edu.au)

\bigskip

{\bf Description}
\medskip

The application of computer algebra techniques to category theory is still relatively little
developed, but in the last five to ten years significant progress has been made, and there is now a
growing group of people working in the field. 

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). 

{\em 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. 

{\em 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. 

{\em 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. 

\bigskip
{\bf Talks}
\medskip

Date: July 18th (Thursday) 

\begin{description}
\item[14:00-14:45 ] \ \\
  Robert Walters
\\
  {\bf The Todd-Coxeter procedure and the computation of left Kan extensions.} 
\item[14:45-15:05 ] \ \\
  Richard Buckland
\\
  {\bf CASE for concurrent systems based on the computer algebra of n-categories.} 
\item[15:05-15:25] \ \\
  Makoto Takeyama
\\
  {\bf Universal structure and categorical reasoning in type theory.} 
\item[15:25-15:45] \ \\
  Robbie Gates\\
  {\bf Generic solutions to polynomial equations in distributive categories.} 
\item[15:45-16:05 ] \ \\
  \\
  {\bf Coffee Break } 
\item[16:05-16:25] \ \\
  Robert Rosebrugh\\
  {\bf Database tools for category theory.} 
\item[16:25-16:45] \ \\
  Ronald Brown\\
  {\bf The Axiom computer algebra system applied to computational
    category theory.} \\
(joint work with W. Dreckmann(Bangor and Stockholm)) 

\item[16:45-15:30] \ \\
  F. William Lawvere\\
  {\bf Graphic toposes, n-categories and resulting problems of
    computer algebra.} 
\end{description}

