*Fibred models of processes*

*by Marcelo Fiore, University of Sussex at Brighton*

**Abstract:**

* TBA*
Path Integrals, Bayesian Vision, and Is Gaussian Quadrature Really Good?

*by Peter Freyd, Univ. of Pennsylvania. *

**Abstract:**

Physicists know how to integrate over all possible paths,
computer-vision experts want to assign probabilities to arbitrary
scenes, and numerical analysts act as if some continuous functions are
more typical than others. In these three disparate cases, a more
flexible notion of integration is being invoked than is possible in
the traditional foundations for mathematics. If allowed to enter a
highly speculative mode, such as the intersection of category theory
and computer science, we may bump into some solutions to the problem.

* Several Applications of Analytic Functors to Theoretical
Computer Science*

*by Ryu Hasegawa, Univ of Tokyo, Japan.*

**Abstract:**

Analytic functors, or combinatorial species, were introduced by
Joyal in 80's to provide a categorical foundation to
enumerative combinatorics. Incidentally we found that analytic
functors can be used as foundations of several subjects in
theoretical computer science.
A famous theorem by Kruskal of well-quasi-ordering finite trees
was employed by Dershowitz in term rewriting systems to develop
the theory of termination orderings. We show that a class of
well-quasi-orderings including Kruskal's and other well-known
examples is generated by considering analytic functors. So we
have a simple uniform method to form classes of
well-quasi-orderings and well-orderings.
Second we consider the theory of lambda calculi. Girard gave
semantics of several systems of lambda calculi by introducing
normal functors, which are, as seen by a minute of thinking,
special cases of analytic functors. So the machinery of
enumerative combinatorics behind analytic functors are useful
to show some properties of the normal functor model.
Furthermore we focus on the fixpoint operators, which are often
used to interpret recursion in computer science. The
Lagrange-Good inversion formula, known in analysis and
enumerative combinatorics, gives an expression for computing
fixpoints of certain recursive definitions on formal power
series. We give a new computer theoretical proof of the
formula, considering the interpretation of the fixpoint operator
in the normal functor model. In the proof, we employ the
recent finding by Hasegawa relating fixpoint operators
with categorical traces of Joyal, Street and Verity.

*Designware: Software Development by Refinement*

*by Douglas R. Smith, Kestrel Institute, Palo Alto, California*

**Abstract:**

This talk presents a mechanizable framework for software
development by refinement. The framework is based on a category of
specifications. The key idea is representing knowledge about
programming concepts, such as algorithm design, datatype refinement,
and expression simplification, by means of taxonomies of
specifications and morphisms.
The framework is partially implemented in the research systems
Specware, Designware, and Planware. Specware provides basic support
for composing specifications and refinements via colimit, and for
generating code via logic morphisms. Specware is intended to be
general-purpose and has found use in industrial settings. Designware
extends Specware with taxonomies of software design theories and
support for constructing refinements from them. Planware builds on
Designware to provide highly automated support for requirements
acquisition and synthesis of high-performance scheduling algorithms.