**Lifting**
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 shall 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 this
does not depend, for instance, on having enough pullbacks.
This approach to partiality seems new in the literature on categories
of partial maps since there the central role 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.
This is joint work with Anna Bucalo.

**Functor categories and partial evaluation**
We propose a semantics in a suitable functor category for a
two-level language in Gomard and Jones (1991). In this semantics
functional types are interpreted in the canonical way (i.e. by
exponentials) and the elements of type *code* are in one-one
correspondence with closed lambda-terms modulo alpha-conversion.
By using functor categories we avoid the pitfalls of the two-level
semantics in Gomard and Jones (1991) , which uses a *newname*
construct with an unclear status.
Functor categories have been proposed by Oles (1985) to model local
variables in Algol-like languages, and used by several researchers for
similar purposes since then. So it is not surprising that they can
model correctly the *newname* construct.

**An abstract Stone duality**
Domain theory is based on the proposal by Dana Scott that topology
be used as an aproximation to recursion theory. At first sight,
the lattice of RE subsets of the natural numbers looks like a topology,
in that it admits finite intersections and some infinitary unions.
Unfortunately the topology (in the standard sense) which this generates
is the discrete one. (There is a difference of intuition between
analysis, where neighbourhoods are small - of size epsilon - and
recursion, where they are big - recursively enumerable.)

In classical domain theory, continuity is given by directed joins.
Turning this on its head, we can replace the troublesome directed
joins in the definition of a topology by continuity, ie by enriching
the theory of locales (lattices of open sets) over spaces. This
circular definition says that the category of spaces is to be dual
to the category of algebras for a certain monad over itself.

I shall show how several concepts from general topology, including
compact Hausdorff spaces, can be presented in this framework, which
I claim gives the unified axiomatisation of topology and recursion.

**Limits in double categories**
We define the notion of (horizontal) double limit for a double functor
F: I -> A between double categories, and we give a construction
theorem for such limits, from double products, double equalisers and
tabulators (the double limits of vertical arrows). Double limits can
describe important tools; for instance, the Grothendieck construction
of a profunctor is its tabulator, in the "double category" of
categories, functors and profunctors. If A is a 2-category, the
previous result reduces to Street's construction theorem of weighted
limits, by ordinary limits and cotensors 2*X (the tabulator of the
vertical identity of X). Double limits are also connected to the
notion of limits "relative to double categories" introduced by
Bastiani-Ehresmann. This is joint work with Robert Paré.

**Two-level languages for program optimization**
We consider the use of 2-level languages in the framework of partial
evaluation. We propose a 2-level version of PCF, and give an operational
and denotational semantics, that give an account of the distinction
between compilation and execution phases. An adequacy theorem is given
to relate the two semantics, and a new denotational model
is introduced to refine the previous one.