**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 <

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