Catálogo de publicaciones - libros

We give a fully abstract game model for Idealized Algol with non-local control flow. In contrast to most previous papers on game semantics, we do not need to include the bad-variable constructor to obtain full abstraction. Using the model we show that, unlike in the “control-free” case, the presence of does affect observational equivalence. We conclude by discussing the effect of on nondeterministic and probabilistic variants of Idealized Algol.

A game semantics of the ( − − *, →)-fragment of the logic of bunched implications, , is presented. To date, categorical models of have been restricted to two kinds: functor category models; and the category itself. The game model is not of this kind. Rather, it is based on Hyland-Ong-Nickau-style games and embodies a careful analysis of the notions of resource sharing and separation inherent in . The key to distinguishing between the additive and multiplicative connectives of is a semantic notion of separation. The main result of the paper is that the model is fully complete: every finite, total strategy in the model is the denotation of a term of the -calculus, the term language for the fragment of under consideration.

The third is presented at this CSL’07. This is the first year in which the EACSL Ackermann Award is generously sponsored. Our sponsor for the next three years is the worlds leading provider of personal peripherals, Logitech S.A., situated in Romanel, Switzerland.