*Proof Principles for Datatypes with Iterated Recursion*

*by Ulrich Hensel, Bart Jacobs*

**Abstract:**

Data types like trees which are finitely branching and of (possibly)
infinite depth are described by iterating initial algebras
and terminal coalgebras. We study proof principles for such
data types in the context of categorical logic, following and
extending the approach
of~[HermidaJ95b,JacobsHermidaIndCoind96].
The technical contribution of this paper involves a description of
initial algebras and terminal coalgebras in total categories
of fibrations for lifted
``datafunctors''. These lifted functors are used to formulate our proof
principles. We test these principles by proving some elementary
results for four kinds of trees
(with finite or infinite breadth or depth) using the proof
tool PVS.

*When do datatypes commute?*

*by Paul Hoogendijk, Roland Backhouse*

**Abstract:**

Polytypic programs are programs that are parameterised by type constructors (like
List), unlike polymorphic programs which are parameterised by types (like Int).
In this paper we formulate precisely the polytypic
programming problem of ``commuting'' two datatypes. The precise
formulation involves a novel notion of higher order naturality. We demonstrate
via a number of examples the relevance and interest of the problem, and we show that
all ``regular datatypes'' (the sort of datatypes that one can define in a functional
programming language) do indeed commute according to our specification. The
framework we use is the theory of allegories, a combination of category theory with the
point-free relation calculus.

*A factorisation theorem for external derivations*

*by Paul-Andre Mellies*

**Abstract:**

Among all the potential computations of a term, some are better than others.
In my PhD, I give an algebraic characterisation of the << good >>
ones, for instance the leftmost outermost reductions of the lambda-calculus:
a derivation e: M -> P is << external >> if e.f: M -> Q
is standard for any standard derivation f: P -> Q.

In this short talk, I will show that every derivation d: M -> Q
can be factorised as an external derivation from e: M -> P
followed by an << internal >> derivation f: P -> Q.
Moreover, this epi-mono factorisation is functorial
(i.e there is a nice diagram) in the sense of Freyd-Kelly.

Conceptually, the factorisation result means that the good part
in a computation can always be separated from the junk.
Technically, it is the key step towards the description of
stability (semantics) as a syntactic phenomenon.
In fact, contrary to usual derivation spaces (see Levy's PhD),
external derivation spaces enjoy meets.

*A decision algorithm for linear isomorphism of types with complexity O(nlog^2(n)).*

*by Alexander Andreev, Sergei Soloviev*

**Abstract:**

It is known, that ordinary isomorphisms (associativity
and commutativity of ``times'', isomorphisms for ``times''
unit and currying) provide a complete
axiomatisation of isomorphism of types in multiplicative linear lambda
calculus (isomorphism of objects in a free symmetric monoidal closed
category). One of the reasons to consider linear
isomorphism of types instead of ordinary isomorphism was that better
complexity could be expected. Meanwhile, no upper bounds reasonnably close
to linear were obtained. We describe an algorithm deciding if two types
are linearly isomorphic with complexity O(nlog^{2}(n)).

*Lifting*

*by A. Bucalo, G. Rosolini*

**Abstract:**

Lifting is the name with which, in semantics of programming languages,
one refers to a representation of partial maps. It relates to the
order induced on the representation by the inclusion of graphs of
partial maps, which usually adds one element below all others. The
problem we want to consider is precisely that of recognizing a lifting
functor in a category, possibly lacking part of the structure required
to define the representation. We solve it in the general case of
a category with a terminal object; this indicates that a lifting
functor carries an imprint which distinguishes it, and does not
depend, for instance, on having pullbacks in the category.

This approach to partiality seems new in the literature on categories
of partial maps since there the central r\^ole is played by the
Kleisli category on the monad: the category of total maps is only
instrumental, and always recognized as definable from that of partial
maps (when this comes with sufficient structure). On the other hand,
it is certainly implicit in the computational point of view, and it
relates directly to the question of modularity: once the structure of
lifting is known, one knows how to mix that with others.

An interesting characterization of lifting is obtained when we
specialize our result to categories with finite products.

*Shedding New Light in the World of Logical Systems*

*by Uwe Wolter, Alfio Martini*

**Abstract:**

The notion of an Institution [GB92] is here taken as the precise
formulation for the notion of a logical system. By using elementary
tools from the core of category theory, we are able to reveal the
underlying mathematical structures lying ``behind'' the logical
formulation of the satisfaction condition, and hence to acquire a
both suitable and deeper understanding of the institution concept.
This allows us to systematically approach the problem of describing
and analyzing relations between logical systems. Theorem 2.11
redesigns the notion of an institution to a purely categorical level,
so that the satisfaction condition becomes a functorial (and natural)
transformation from specifications to (subcategories of) models and
vice versa. This systematic procedure is also applied to discuss and
give a natural description for the notions of institution morphism and
institution map. The last technical discussion is a careful and
detailed analysis of two examples, which tries, as an outcome,
to outline how the new categorical insights could help in guiding
the development of a unifying theory for relations between logical
systems.

*Effectiveness of the Global Modulus of Continuity on Metric Spaces*

*by Klaus Weihrauch, Xizhong Zheng*

**Abstract:**

Abstract: Let (X,d_X) and (Y,d_Y) be metric spaces. By definition, there is a function h which maps every triple (f,x,\epsilon) to \delta > 0, for any continuous function f from X to Y, element x in X and real \epsilon > 0, such that d_Y(f(x), f(x')) < \epsilon whenever d_X(x,x') < \delta for all x' in X. Such a function h is called the global modulus of continuity on the function space C(X,Y) of continuous functions from X to Y. By a recent result of Repovs and Semenov, there is a continuous global modulus of continuity on C(X,Y), if X is locally compact. Their proof applies the classical Selection Theorem of Michael, i.e., h exists as a selection function of some lower semi continuous set valued function. Thus it is quite ineffective. Based on Weihrauch's frameworks on computable metric space, we effectivize this result. A computable metric space X of Weihrauch's sense is called effectively locally compact, if we can determine effectively from any element x of X a compact neighbourhood B(x
) of x. Our main theorem of this paper says that there is a computable global modulus of continuity on C(X,Y) if X is a effectively locally compact metric space. Our proof is a direct construction of an algorithm which computes the global modulus of continuity.

*Monads and Modular Term Rewriting*

*by Christoph Lueth, Neil Ghani*

**Abstract:**

Monads can be used to model term rewriting systems by generalising
the well-known equivalence between universal algebra and monads on
the category Set. In [Lu96], the usefulness of this
semantics was demonstrated by giving a purely categorical proof of
the modularity of confluence for the disjoint union of term
rewriting systems (Toyama's theorem). This paper provides further
support for the use of monads in term rewriting by giving a
categorical proof of the most general theorem concerning the
modularity of strong normalisation. In the process, we also improve
upon some technical aspects of the earlier work.

[Lu96] Compositional Term Rewriting: An algebraic proof of Toyama's
theorem. RTA'96, Springer LNCS 1103.

*Presheaf Models for the pi-Calculus*

*by Gian Luca Cattani, Ian Stark, Glynn Winskel*

**Abstract:**

Recent work has shown that presheaf categories provide a general model of
concurrency, with an inbuilt notion of bisimulation based on open maps. Here
it is shown how this approach can also handle systems where the language of
actions may change dynamically as a process evolves. The example is the
\pi-calculus, a calculus for `mobile processes' whose communication topology
varies as channels are created and discarded. A denotational semantics is
described for the \pi-calculus within an indexed category of profunctors;
the model is fully abstract for bisimilarity, in the sense that bisimulation
in the model, obtained from open maps, coincides with the usual bisimulation
obtained from the operational semantics of the \pi-calculus. While
attention is concentrated on the `late' semantics of the \pi-calculus, it is
indicated how the `early' and other variants can also be captured.

*Categorical Modelling of Structural Operational Rules: case studies*

*by Daniele Turi*

**Abstract:**

This paper aims at substantiating a recently introduced
mathematical theory of `well-behaved' operational
semantics by applying it to a significant variety of
examples. These involve: non-determinism, interaction,
side-effects, exceptions, and trace equivalence.
Both guarded and unguarded recursive programs are
also treated, the former using a novel functorial notion
of guardedness and the latter by working in categories
of partial maps.

*A 2-Categorical Presentation of Term Graph Rewriting*

*by Andrea Corradini, Fabio Gadducci*

**Abstract:**

It is well-known that a term rewriting system can be
represented faithfully as a cartesian 2-category, where
horizontal arrows represent terms, and cells represent rewriting
sequences. In this paper we propose a similar, original
2-categorical representation for term graph rewriting.
Building on a result recently presented by the authors, which shows
that term graphs over a given signature are in one-to-one
correspondence with arrows of a ps-monoidal category freely
generated from the signature, we associate with a term graph
rewriting system a ps-monoidal 2-category, and show that
cells faithfully represent its rewriting sequences. We also
discuss how to deal with garbage collection, and we exploit the
categorical framework to relate term graph rewriting and term
rewriting. This last point is based on the observation that
ps-monoidal (2-)categories can be regarded as "weak" cartesian
(2-)categories, where certain naturality axioms have been
dropped.

*Combining and Representing Logical Systems*

*by Till Mossakowski, Andrzej Tarlecki, Wieslaw Pawlowski*

**Abstract:**

The paper addresses important problems of building complex logical
systems and their representations in universal logics in a systematic
way. Following Goguen and Burstall, we adopt the model-theoretic view
of logic as captured in the notion of institution and of parchment (a
certain algebraic way to present institutions).

We propose a modified notion of parchment together with a notion of
parchment morphism and representation, respectively. We lift formal
properties of the categories of institutions and their representations
to this level: the category of parchments is complete, and parchment
representations may be put together using categorical limits as
well. However, parchments provide a more adequate framework for
systematic combination of logical systems than institutions. We
indicate how the necessary invention for proper combination of various
logical features may be introduced either on an ad hoc basis (when
putting parchments together using limits in the category of
parchments) or via representations in a universal logic (when
parchment combination is driven by their representations).

*General Synthetic Domain Theory -- A Logical Approach (Extended abstract)*

*by Bernhard Reus, Thomas Streicher*

**Abstract:**

Synthetic Domain Theory (SDT) is a version of Domain Theory
where ``all functions are continuous''.
In the first author's Thesis there has been developed a logical and
axiomatic version of SDT which is special in the sense that it captures the
essence of Domain Theory `a la Scott but rules out e.g. Stable Domain
Theory as it requires that the order on function spaces is pointwise.
In this article we will give a logical and axiomatic account of
a general SDT aiming to grasp the structure common to all notions of
domains which has been advocated by many authors.
As in loc.cit. the underlying logic is a sufficiently expressive
version of constructive type theory.
We start with a few basic axioms giving rise to a core theory on top of
which we study various notions of predomains as e.g. complete and
well-complete
S-spaces, define the appropriate notion of domain and prove
the common induction principles.

*Specifying Interaction Categories*

*by Dusko Pavlovic, Samson Abramsky*

**Abstract:**

We analyse two complementary methods for obtaining models of typed
process calculi, in the form of interaction categories. These methods
allow adding new features to previously captured notions of process
and of type, respectively. By combining them, all familiar examples of
interaction categories, as well as some new ones, can be built
starting from some simple familiar categories.

Using the presented constructions, interaction categories can be
analysed without fixing a set of axioms, merely in terms of the way in
which they are specified --- just like algebras are analysed in terms
of equations and relations, independently on abstract
characterisations of their varieties.

*A Calculus for Collections and Aggregates*

*by Kazem Lellahi, Val Tannen*

**Abstract:**

We present a calculus that should play for database query languages
the same role that the lambda calculus plays for functional
programming. For the semantic foundations of the calculus we introduce
a new concept: monads enriched with algebraic structure. We model
collection types through enriched monads and aggregate operations
through enriched monad algebras. The calculus derives program
equivalences that underlie a good number of the optimizations used in
query languages.