 | |
Sessions
take place in auditorium 3 unless otherwise indicated.| 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. |
| 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. |
| 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. |
| 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. |
Room:
Restaurant Langelinie Pavillonen | |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
