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.