We decided to take advantage of the concurrent visits of Hitoshi Ohsaki, Nguyen Van Tang,
and Takashi Kitamura to run a fourth workshop at the University of Bath on the afternoon
of 17 March 2010. The details are as follows:
14.15-14.45: Ana Calderon
15.15- 16.30 Hitoshi Ohsaki
16.30- 16.45 Break (If needed)
16.45- 17.30 Guy McCusker
Titles and Abstracts:
Title: Tree Automata for Non-Linear Arithmetic
Tree automata modulo associativity and commutativity axioms, called AC tree
automata, accept trees by iterating the transition modulo equational reasoning.
The class of languages accepted by monotone AC tree automata is known to include
the solution set of the inequality x * y >= z, which implies that the class properly
includes the AC closure of regular tree languages. In the talk, we characterize more
precisely the expressiveness of monotone AC tree automata, based on the
observation that, in addition to polynomials, a class of exponential constraints (called
monotone exponential Diophantine inequalities) can be expressed by monotone AC tree
automata with a minimal signature. Moreover, we show that a class of arithmetic logic
consisting of monotone exponential Diophantine inequalities is definable by monotone AC
tree automata. The results presented in the talk are obtained by applying our novel
tree automata technique, called linearly bounded projection. This talk is based on our
paper (with Naoki Kobayashi, Tohoku University) at RTA 2008
and my lecture note presented at ISR 2009 (http://isr09.cic.unb.br/).
Title: Understanding Game Semantics through Coherence Spaces
Abstract: Game Semantics has successfully provided fully abstract
models for languages, not possible using other denotational approaches.
Although it is a flexible and accurate way to give semantics to a
language, its underlying mathematics is awkward. For example, the
proofs that strategies compose associatively and maintain properties
imposed on them such as innocence are intricate and require a lot of
attention. This work aims at beginning to provide a more elegant and
uniform mathematical ground for Game Semantics.
Our quest is to find mathematical entities that will retain the
properties that make games an accurate way to give semantics to
programs, yet that are simple and familiar to work with. Our main
result is a full, faithful strong monoidal embedding of a category of
games into a category of coherence spaces, where composition is simple
composition of relations.
Title: Modelling local variables: possible worlds and object spaces
Abstract: Local variables in imperative languages have been given
denotational semantics in at least two fundamentally different ways. One
is by use of functor categories, focusing on the idea of possible worlds.
The other might be termed event-based, exemplified by Reddy's
object spaces and models based on game semantics. O'Hearn and Reddy
have related the two approaches by giving functor category models
whose worlds are object spaces, then showing that their model is fully
abstract for Idealised Algol programs up to order two. But the
category of object spaces is not small, and so their functor category
is unlikely to be locally small. That means they cannot use the body
of results flowing from local smallness, such as cartesian closedness
of the functor category and its implications for their model. In this
talk we show how to refine their model by proving that the finite
objects form a small dense subcategory of a simplified object-spaces model,
making the induced functor category locally small, at the expense of being
forced to work in a Cpo-enriched setting.
Nguyen Van Tang