ABSTRACT. We present a Geometry of Interaction model for higher-order computation which has the ability to model commutative effects in a parallel setting, and in particular to capture probabilistic and quantum effects. The model comes with a multi-token machine, a proof net system, and a PCF-style language. Being based on a rewrite system equipped with a memory, it has a concrete nature which makes it well suited for building low-level operational descriptions of higher-order languages. A success of this approach is to give (essentially for free) an adequate model for a fully-fledged quantum programming language in which entanglement, duplication, and recursion are all available.

A question which is key to our results is the following: What become the notions of confluence and convergence when a parallel rewrite system has both a probabilistic choice and the possibility of non-termination?

Joint work with Ugo Dal Lago, Benoit Valiron, Akira Yoshimizu

ABSTRACT. We introduce a geometry of interaction model for Mazza's multiport interaction combinators, a graph-theoretic formalism which is able to faithfully capture concurrent computation as embodied by process algebras like the π-calculus. The introduced model is based on token machines in which not one but multiple tokens are allowed to traverse the underlying net at the same time. We prove soundness and adequacy of the introduced model. The former is proved as a simulation result between the token machines one obtains along any reduction sequence. The latter is obtained by a fine analysis of convergence, both in nets and in token machines.

Joint work with Ryo Tanaka and Akira Yoshimizu

ABSTRACT. Girard's geometry of interaction (GoI) can be seen as a compositional compilation method from functional programs to sequential machines, where tokens move around and express interactions between (parts of) programs. Intrigued by the combination of abstract theory and concrete dynamics in GoI, our line of work (with Naohiko Hoshino, Koko Muroya and Toshiki Kataoka) has aimed at exploiting, in GoI, results from the theory of coalgebra---a categorical abstraction of state-based transition systems that has found its use principally in concurrency theory. Such reinforced connection between higher-order computation and state-based dynamics is made possible thanks to an elegant categorical axiomatization of GoI by Abramsky, Haghverdi and Scott, where traced monoidal categories are identified to be essential in modeling interaction. In the talk I shall lay out these basic ideas, together with some of our results on: GoI semantics for a quantum programming language; and extension of GoI with algebraic effects.

ABSTRACT. Although Plotkin’s parallel-or is inherently deterministic, it has a non-deterministic interpretation in games based on (prime) event structures – in which an event has a unique causal history – because they do not directly support disjunctive causality. General event structures can express disjunctive causality and have a more permissive notion of determinism, but do not support hiding. We show that (structures equivalent to) deterministic general event structures do support hiding, and construct a new category of games based on them with a deterministic interpretation of an affine variant of PCF extended with parallel-or. We then exploit this deterministic interpretation to give a relaxed notion of determinism (observable determinism) on the plain event structures model. Putting this together with our previously introduced concurrent notions of well-bracketing and innocence, we obtain an intensionally fully abstract model for our language.

This is joint work with Simon Castellan and Glynn Winskel, presented at FSCD 2017.

ABSTRACT. In many game models, including the AJM and HO/N models, a strategy can be represented as a subset of the set of all plays of an appropriate type. The collection of plays is, however, not a mere set but that equipped with symmetry, which every strategy should respect. Actually the set of plays of a game in the AJM model is explicitly associated with an equivalence relation. As for the HO/N model, Mellies studied an equivalence relation on plays that every innocent strategy respects.

In this talk, we study the situation by using ideas from combinatorics, namely generalised species and profunctors. We show that the collection of all plays of a given simple type can be seen as a generalised species or a profunctor, and that this mapping induces a (pseudo)functor from the game model to the bicategory of profunctors.

(This is joint work with Kazuyuki Asada and C.-H. Luke Ong.)

ABSTRACT. This talk will review probabilistic concurrent strategies (based on event structures), their definition and properties, and indicate issues and topics for future work.

ABSTRACT. This talk will examine the role of game semantics as a bridge between operational and denotational semantics, combing the computational insights of the former with the good mathematical properties of the latter, especially compositionality.

ABSTRACT. While most game models feature a rather intuitive setup, they also come with surprisingly difficult proofs of such basic results as associativity of composition of strategies.  We propose a basic abstract framework for game semantics, (innocent) game settings, which enables the generic construction of a category of games and (innocent) strategies, thus unifying a number of concrete cases.

ABSTRACT. Game semantics has been developed since the 1990's as a denotational paradigm capturing observational equivalence of functional languages with imperative features. While initially introduced for PCF variants, the theory can nowadays express effectful languages ranging from ML fragments and Java programs to C-like code. In this talk we present recent advances in devising game models for effectful computation. Central in this approach is the use of names for representing in an abstract fashion different forms of notions and effects, such as references, higher-order values and polymorphism. Moreover, the use of names facilitates the presentation of game moves as method calls and returns, thus transforming games from a denotational semantics to an operational/trace semantics for open terms.

ABSTRACT. Probabilistic strategies were first introduced by Danos and Harmer in a probabilistic extension of Hyland-Ong games. They work particularly well for modelling probabilistic programs with state: the model is fully abstract for a probabilistic variant of Idealised Algol. Recently, concurrent games were introduced as an alternative framework for game semantics, based on event structures, a fundamental model for concurrent processes. Concurrent games can also be enriched with probability, using a notion of probabilistic event structure, and this makes possible an analysis of Probabilistic PCF (including an intensional full abstraction result).

However all the above do not readily support continuous distributions, making those models unsatisfactory for practical probabilistic languages, in which such distributions are essential. Vakar and Ong have recently announced a generalisation of the Danos-Harmer model, which supports continuous distributions. They also describe an application to a stateful probabilistic language. Here we present a new probabilistic concurrent games model in which strategies are equipped to support arbitrary distributions on the real numbers. We rely on methods of measure theory and introduce measurable event structures, which generalise event structures and form the basis for a model of measurable concurrent games. Then one may adjoin probability in the form of a family of stochastic kernels. We illustrate the model by giving semantics to a higher-order, affine version of Probabilistic PCF with continuous distributions on the reals.

ABSTRACT. In previous work, presented at GaLoP 2018, we have defined an adequate game semantics for the linear quantum lambda calculus. To do this we drew inspiration on two lines of work. On the one hand, our account of the dynamics of computation came from the concurrent games on event structures of Winskel et al, and their extension with probabilistic annotations (which we extend conservatively). On the other hand, our formulation of quantum states was inspired by the work of Pagani, Selinger and Valiron about static denotational semantics for the quantum λ-calculus. We used for games event structures annotated by Hilbert spaces, and we annotated the strategies by operators on those Hilbert spaces.

In this work, we present a notion of (sequential) quantum innocence, leading to a definability result with respect to the linear quantum lambda-calculus. Quantum innocence imposes a compatibility between quantum annotations and the causal structure of strate- gies, ensuring that they can be reproduced by terms. We obtain a fully abstract model for the linear quantum λ-calculus. This is not the first fully abstract model in the linear case, see [8] by Selinger and Valiron. However, there is not yet any fully abstract model for the non linear case. Following the work on event structures with symmetry in by Castellan , Clairambault, Paquet and Winskel for probabilistic PCF, we expect to be able to extend it into a fully abstract model for the (full) quantum λ-calculus.

Interestingly, the work on definability lead us to a more abstract definition of quantum games and strategies, relying only weakly on the properties of quantum annotations. Though this is work in progress, it seems to lead to a fully abstract games model for a linear λ-calculus parametrised by a symmetric monoidal category.

ABSTRACT. In the study of programming languages, denotational semantics is used to abstract away from (some) intermediate steps of computation, in particular by hiding/internally handling the process of composition of λ-calculi. Although these abstractions are very useful to help reasoning about program behaviours such as program termination, they are often too strong to be able to reflect some quantitative information, or meta-data, such as permissions, time, or energy consumption, that can be of interest for program analysis and optimisation.

In this work we present a framework of annotated concurrent games based on event structures that generally allows for keeping track of meta data, that is, information whose value may vary with the execution flow but cannot modify it. More precisely, for a given equational theory, we build a compact closed category of concurrent games and strategies in which Player moves come equipped with expressions that may only depend on variables representing Opponent moves from their causal history. These expressions may indicate resources required to reach these events, for instance in terms of permissions or time. The free variables corresponding to Opponent moves in these expressions reflect the fact that resource usage may depend on what Opponent already requires; they are instantiated while performing the composition of the strategy with its environment.

In a second time, we use this new framework to give a denotational semantics of an affine IPA-style language with explicit time consumption (or any resource that fits in a concurrent monoid(R, ⋆, ; , 0, ≤) with distributive law a; (b ⋆ c) = (a; b) ⋆ (a; c)) in the spirit of Ghica’s slot games. We show that this interpretation is sound with respect to the usual interleaving-based operational semantics, and (unlike slot games) with respect to its extension allowing non-interfering parallel computation. Even with this extension, however, adequacy does not hold: in essence, our semantics predicts resource usage for the most parallel execution possible, with no scheduling or allocation constraints.

ABSTRACT. I will give a survey of various classes of automata that have been used to capture the game semantics of higher-­order programs and, consequently, obtain decidability results for contextual equivalence.