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.