DOMAIN on Saturday

Detailed program
Saturday July 20th, 2002
See also the unified by-slot program

Sessions take place in auditorium 3 unless otherwise indicated.

Session 1

09:00-10:00  Martin Hyland, U Cambridge, UK
Invited talk: Thirty years on! domain models for lambda calculus: the categorical logic perspective
We explain the categorical logic reading of intersection-type theories, and describe the corresponding generic models. We apply these ideas to models of various versions of ludics.

10:00-10:30  Gordon Plotkin, U Edinburgh, UK
John Power, U Edinburgh, UK
Computational effects and operations: an overview
We overview a programme to provide a unified semantics for computational effects based upon the notion of a countable enriched Lawvere theory. We define the notion of countable enriched Lawvere theory, show how the various leading examples of computational effects, except for continuations, give rise to them, and we compare the definition with that of a strong monad. We outline how one may use the notion to model three natural ways in which to combine computational effects: by their sum, by their commutative combination, and by distributivity. We also outline a unified account of operational semantics. We present results we have already shown, some partial results, and our plans for further development of the programme.

Session 2

11:00-12:00  John C. Reynolds, Carnegie Mellon U, USA
Invited talk: Relating intrinsic and extrinsic semantics in domain theory
A definition of a typed language is said to be "intrinsic" if it assigns meanings to typings rather than arbitrary phrases, so that ill-typed phrases are meaningless. In contrast, a definition is said to be "extrinsic" if phrases have the same meaning as in a typeless semantics, while typings represent properties of these untyped meanings (more precisely, PER's on the set of untyped meanings).
Using domains, it is straightforward to give intrinsic, typeless, and extrinsic semantics for many versions of the typed lambda calculus. We will describe the relationship between these semantics and, in particular, show that one can move, from intinsic semantics that are connected with untyped semantics via logical relations, to extrinsic semantics, and vice-versa.

12:00-12:30  Lee Flax, Macquarie U, Australia
Approximation of entailment
In the interest of approximating the computation of entailment in first-order logic, restricted entailments are defined. A restricted entailment is a generalisation of ordinary entailment obtained when model checking of sets of sentences is restricted to a subset of all structures defined on the vocabulary of the language. The set of restricted entailments forms a domain which contains ordinary entailment as a member. The compact members of the domain are characterised, and it is shown that any restricted entailment whose restriction is a finite set of structures, is compact. So ordinary entailment is approximated by restricted entailments with finite restrictions. In the conclusion some remarks are made about the effective computation of restricted entailment.

Session 3

14:00-15:00  Pierre-Louis Curien, U Paris VII, France
Invited talk: Playful computation
We survey works of the last two decades or more tending to approach the semantics of prograqmming languages from an interactive point of view: from Berry-Curien's sequential algorithms to Girard's ludics through game semantics. Other branches converge to this line of research: Kleene's oracles, Lorentzen's dialogue games.

15:00-15:30  Panagis Karazeris, U Patras, Greece
Jirí Velebil, Techn. U of Braunschweig, Germany
Left exact Kan extensions, powerdomain distributivity, preservation of bisimulation
We examine completions of small categories under finite colimits. We focus on completions of those categories that satisfy a weak completeness property, which constitutes a categorical analogue of coherence in traditional domain theory. The property in question is that for any diagram inside the category the cone functor for it is a finite colimit of representable ones. It is further equivalent to the fact that the completion of the category under finite colimits has finite limits. We examine the left exactness of finite colimit preserving functors that are induced by the universal property of the completion. We show that the finite colimit completion monad on small categories lifts to one on small categories with finite limits. This amounts to a distributivity law between upper and lower powerdomain constructions at the level of accessible categories (qua generalized domains). We commend on the fundamental result of Cattani and Winskel that colimit preserving functors preseve bisimulation from the perspective of the above results.

Session 4

16:00-16:30  Jirí Adámek, Techn. U of Braunschweig, Germany
On a description of free iterative theories
For a polynomial endofunctor H of Set, a free iterative theory on H has been described by Elgot and his coauthors: it is the theory of rational trees. Here we describe free iterative theories on all finitary endofunctors of Set as quotient theories of the rational-tree theories.

16:30-17:30  Martín Escardó, U Birmingham, UK
Invited talk: Interactions between domain theory and topology
This will be a survey of the fruitful interaction of domain theory and topology, including function spaces, injective spaces, and various kinds of topological algebras. It will include old and recent results, some with applications to domain theory and others with applications to topology.

19:00-23:00  DOMAIN dinner

Room: Restaurant Langelinie Pavillonen