Abstracts

The topos of 3-colored graphs The problem of 3 coloring finite undirected graphs is NP-complete and therefore there is interest in the structure of graphs which are and are not 3 colorable. The category of undirected graphs U is a topos. A graph with a given 3 coloring is said to be 3-colored. The category C of 3-colored graphs is is a cocomplete topos, hence also complete. There is an essential geometric morphism between U and C, and the three functors involved have considerable natural appeal. These functors justify two of the heuristics used to quicken algorithms which determine whether or not a 3 coloring exists for argument finite undirected graphs. Indeed, one of these heuristics deserves to be better known.
In addition, there is another pair of adjoint functors between C and U. Finally, we give the Heyting algebra structure of the subobject classifier for C, this being the ``internal logic''of C.

Type theory via exact categories Partial equivalence relations (and categories of these) are a standard tool in semantics of type theories and programming languages since they often provide a cartesian closed category with extended definability. Using the theory of exact categories, we give a category-theoretic explanation of the reason the construction of a category of partial equivalence relations often produces a cartesian closed category. We show how several familiar examples of categories of partial equivalence relations fit into the general framework. This work is based on the seminal work of Dana Scott on models of the lambda-calculus, and it is joint with him, his student Lars Birkedal, and Aurelio Carboni. We shall draw comparisons with various other works on these categories.

Varieties with Self In ``A Theory of Objects'', Abadi and Cardelli propose a type <> whose semantical values, informally, are pairs (C,c) with C a subtype and c a value of the subtype. We take this informal description seriously, to obtain, for each type of universal algebra, or variety, T, another type of variety Self(T), whose values are exactly such pairs (C,c) with C a subtype of T and c a model of C, that is, an algebra of variety C. This means that we are considering only the algebraic aspects of objects, but this gives already considerable technicalities which are rather different than in usual approaches to universal algebra. This talk presents joint work in progress with Jiri Rosicky.

Enriched accessible categories For instance, what is an accessible 2-category? It is certainly not a 2-category such that the underlying category is accessible. We propose a specific definition and show the equivalence with the notion of a category of models of an enriched sketch, or that of a category of enriched flat functors.

Sketch Tensor Products for Computer Science General sketches, also called mixed sketches, offer a syntactic variant to first order logic which is used to compactly describe data structures. Sketch tensor products enable us to easily describe one type of data structure interpreted in the models of another, and when the order of this interpretation may be reversed to give the same class of models.
Fundamentally, such nice results occur when the limits and colimits specified by one sketch commute with the colimits and limits specified by the other. For instance, connected limits commute with coproducts in SETS.
This gives us a means for treating programs-as-data: The sketches for program semantics have to have limit and colimit specifications commuting with the colimit and limit specifications of sketches for data. Similarly, independent portions of the data in simulation frameworks need to have the same commutaiton structure.
These concepts immediately indicate the importance of the family construction, which from results in Makkai and Paré, changes the limit specification in a sketch s to a connected limit specification in the sketch s+ of families for s.
The result is that since most computer science data structures can be sketched within the setting of (product, coproduct)-sketches, ideally program semantics ought to be sketched within the framework of (connected limit, epi)-sketches, provided the base category is SETS.
Several variations on this theme will be mentioned, since one can consider families of data structures, etc.
This talk is based on the technical results in ``Multilinearity of Sketches'', Theory and Applications of Categories, 1997, but concentrates on the applications rather than the technical details of sketch tensor product theory.

Topological representation of the lambda-calculus The lambda-calculus can be represented topologically by assigning certain spaces to the types and certain continuous maps to the terms. Using a recent result from category theory, the usual calculus of lambda-conversion is shown to be deductively complete with respect to such topological semantics. It is also shown to be functionally complete, in the sense that there is always a ``minimal'' topological model, in which every continuous function is lambda-definable. These results subsume earlier ones using cartesian closed categories, as well as those employing so-called Henkin and Kripke lambda-models.

Categorical semantics for multistage programming languages First I will give some motivations and examples for multistage programming, and recall a simplified version of METAML (taken from [TBS98]). The rest of the talk will introduce a categorical model, a "semantic-driven" metalanguage, and explain how METAML can be translated into the the metalanguage. If time remains, I may continue with some remarks about encapsulation of effects and existential types.

A category of sequential domains/Full abstraction via realisability The last years there have been several accounts of constructing fully abstract models for PCF without any reference to syntax. Most well known are those based on game semantics where one constructs so-called "intensionally fully abstract" models which turn out to be isomorphic to models whose elements are in 1-1-correspondence with infinite normal forms of PCF terms. The extensional collapse of these game models is a fully abstract model of PCF.
Instead of making a detour via an "intensionally fully abstract model" one may construct a category of cpos with additional relational structure which morphisms are required to preserve besides being continuous.
In the first talk, we present such a category S of sequential domains and show that it allows to interpret all domain constuctors such as lifting, coalesced sum and coalesced product. Furthermore, it is closed under inverse limits which allows one to interpret recursive types.
One may show that for non-recursive types all elements are denotable by a sequential programming language SFL, i.e. lambda-calculus with constructors and eliminators (like let-constructs in ML). From this it follows that SFL with recursive types has a fully abstract model in S. This is joint work with M. Marz.
In the second talk, we show that the fully abstract model of PCF a la Milner arises as a realisability model over the partial combinatory algebra (pca) as given by the solution of the domain equation

A = N_{\bottom} + [A --> A]_{\bottom}.

Let L be the language naturally associated with this domain equation, namely untyped lambda-calculus with arithmetic. One may consider the sub-pca B of A consisting of those elements of A which can be denoted by a closed term of L. The ensuing realisability model Mod(B) can be shown to provide a (non-complete) fully abstract model of PCF which appears as a restriction of the model in Mod(A) to elements realisable by elements of A that can be expressed in L, i.e. we get a notion of computability for elements of the fully abstract model.
Finally, we observe that instead of B we might take any pca of the form L/T where T is a theory containing the (obvious) conversion theory for L and itself being containEd in Th(A). This may be considered as a solution of (a variant of) the Longley-Phoa Conjecture claiming that realisability over a term model of untyped lambda-calculus gives rise to a fully abstract model of PCF.