ABSTRACT. In this survey talk, we revisit the framework of operational game semantics initiated by Soren Lassen.

In contrast to traditional game semantics of programming languages that exposes the constraints on the inhabitants of types, this study provides little or no information on the type structure. However, operational game semantics comes equipped with a proof principle, namely open bisimulation, to study the equality of programs.

We will examine the application of operational game semantics to two non-traditional applications: aspect oriented languages and layout randomization.

Based on joint work with Corin Pitcher, Julian Rathke and James Riely

ABSTRACT. Besides its origins in logic, game semantics has also a well known operational aspect. We outline some of the early operational intuitions behind the full abstraction for PCF, some follow-up algorithmic ideas and some reflections on possible future developments.

ABSTRACT. Although the HO/N games are fully abstract for PCF, the traditional notion of innocence, which underpins these games, is not satisfactory for such language features as nondeterminism and probabilistic branching. Based on a category of P-visible plays with a notion of embedding as morphisms, we propose a natural generalisation by viewing innocent strategies as sheaves over (a site of) plays, echoing a slogan of Hirschowitz and Pous. Our approach gives rise to fully complete game models in a variety of cases, including deterministic, nondeterministic and probabilistic branching. 
 

This is based on joint work with Takeshi Tsukada.

ABSTRACT. This talk presents the following aspects of game semantics.

Game models of higher-order languages can be seen as reflecting CPS, where a move represents a function call. More specifically, the CPS transform from call-by-push-value translates two kinds of computation into a function call: forcing a thunk, and returning a value. These give rise to the two kinds of move: question and answer. But how should such a correspondence be formulated? In recent years, many authors have given transition systems to describe the operational behaviour that the game semantics is supposed to capture. We consider two questions concerning these. Firstly, transition systems may be more precisely described as coalgebras; so we consider what the functors are. And secondly, whereas the transition system usually studied in this context is open (normal form), there are other forms of bisimulation used for operational reasoning, viz. applicative and environmental, so we consider how these too might be related to game semantics.

ABSTRACT. The strategies which represent programs or proofs in game semantics typically do not have access to the full history of play when making their choices. Game theorists recaognise this as the concept of games of imperfect information. An alternative notion of partial information, known as incomplete information, is much less commonplace in game semantics. In this talk we consider the notion of incomplete information, that is, a lack of information about the game itself, in the setting of game semantics of linear logic. Exploiting Harsanyi's reduction of incomplete information to partial information about the payoff structure of games, we show that this incompletness constraints strategies to exhibit a kind of uniformity in their choice of moves, which entails a full completeness result for multiplicative linear logic, replaying Abramsky and Jagadeesan's result of 25 years ago.

ABSTRACT. The notion of asynchronous game was introduced fifteen years ago in order to investigate the causal structure of innocent strategies in game semantics. Shifting from traditional sequential games to asynchronous games was the critical step behind the discovery of a number of structural properties of games and logic. This includes a truly concurrent formulation of innocence based on local confluence diagrams, and a positionality theorem for innocent strategies. Asynchronous games also played a central role in the emergence of tensorial logic as the logic of dialogue games, in the same way as linear logic is the logic of proof nets. Since its origins, one guideline of the theory has been the observation that asynchronous games and asynchronous strategies are causal structures of the very same nature: in other words, asynchronous strategies are asynchronous games themselves, appropriately mapped into other asynchronous games. In this talk, I will develop this simple idea one step further, and explain how to recover and to compare a number of game semantics with different flavors (alternating and non alternating) from the same categorical combinatorics, performed in the category of small categories.

ABSTRACT. Type theory and game semantics are both foundational and practically applicable theories of meaning for programming languages and logics. Indeed, types are at the heart of game semantics, which typically identifies them with games themselves, although moving beyond simple type theory can be challenging. I will give an overview of research into the game semantics of richer typing systems, such as those characterised by Barendregt's "lambda-cube", including:

* Polymorphism: generic models of System F and their extension with subtype polymorphism and bounded quantification. * Dependent Types: recent work developing semantics of Martin-Löf dependent type theory, and extending it with "semantic universes" by relating intensional and extensional models. * Type-operators: some steps towards the semantics of higher-order polymorphism (i.e. quantification over type-operators), which are used in interpreting modules, datatype generic programming and generalised algebraic datatypes.

ABSTRACT. In [Abr05], S. Abramsky introduced various linear/affine combinatory algebras consisting of partial involutions over a suitable formal language, in order to discuss reversible computation in a game-theoretic setting. These algebras arise as instances of the general paradigm explored by E. Haghverdi, called "Abramsky's Programme" [Hag00,AHS02], which amounts to defining a lambda-algebra starting from a GoI Situation in a traced symmetric monoidal category.

In this paper, we investigate this construction from the point of view of the model theory of lambda-calculus. We focus on the strictly linear and the strictly affine parts of Abramsky's Affine Combinatory Algebras. Finally, we briefly outline how to encompass the full algebra.

The gist of our approach is that the GoI interpretation of a term based on involutions is "dual" to the principal type of the term, with respect to the simple types discipline for a linear/affine lambda-calculus. In the general case the type discipline and the calculus need to be extended, respectively, with intersection and !-types, and !-abstractions.

Our analysis unveils three conceptually independent, but ultimately equivalent, accounts of application in the lambda-calculus: beta-reduction, the GoI application of involutions based on symmetric feedback (Girard's Execution Formula), and unification of principal types.

Our result provides an answer, in the strictly affine case, to the question raised in [Abr05] of characterising the partial involutions arising from bi-orthogonal pattern matching automata, which are denotations of affine combinators, and it points to the answer to the full question. Furthermore, we prove that the strictly linear combinatory algebra of partial involutions is a strictly linear lambda-algebra, albeit not a combinatory model, while both the strictly affine combinatory algebra and the full affine combinatory algebra are not. In order to check all the necessary equations involved in the definition of affine lambda-algebra we implement in Erlang application of involutions.

[Abr05] S. Abramsky, "A Structural Approach to Reversible Computation", Theoretical Computer Science, vol. 347 (2005), no.3, pp. 441-464. [AHS02] S. Abramsky, E. Haghverdi, P. Scott, "Geometry of Interaction and linear combinatory algebras", Mathematical Structures in Computer Science, vol. 12 (2002), no.5, pp. 625--665. [Hagh00] E. Haghverdi, "A Categorical Approach to Linear Logic, Geometry of Proofs and full completeness", PhD Thesis, University of Ottawa, 2000.

Joint work with Alberto Ciaffaglione, Furio Honsell, Ivan Scagnetto (University of Udine, Italy)

ABSTRACT. I will explore the idea that if L is a sublanguage of L', it may happen that the observational equivalence relations of L and L' are both hard to analyse, but that L'-observational equivalence for L-terms is relatively tame. For example, we know from game semantics that if L is PCF, then in fact many different extensions L' all yield the same well-understood equivalence relation on L, namely equality of innocent strategies, or equivalently of PCF Böhm trees.

I will discuss various ways of analysing and axiomatizing this equivalence, and present a general theorem showing that any language L' satisfying some mild conditions will give rise to this equivalence on PCF terms.