News

May 20: The group photo will be taken tomorrow, May 21st, after lunch. Let's gather at 1.30pm at the reception.

May 19: The meeting starts at 7pm, with a welcome banquet taking pace in the Azalea room (1st floor).

May 19: Two participants (Olivier Laurent and Luke Ong) unfortunately canceled their participation at the last minute. 

Organizers

Ugo Dal Lago (University of Bologna, Italy)

Claudia Faggian (Université Paris-Diderot, France)

Naohiko Hoshino (Sojo University, Japan)

Participants

Kazuyuki Asada (Tohoku University, Japan)

Kostia Chatdonnet (Loria, France)

Pierre Clairambault (CNRS, Aix-Marseille Université, France)

Ugo Dal Lago (University of Bologna, Italy)

Pietro Di Gianantonio (University of Udine, Italy)

Claudia Faggian (CNRS, Université Paris Cité, France)

Yosuke Fukuda (Kyoto Tachibana University, Japan)

Makoto Hamana (Gunma University, Japan)

Masahiro Hamano (School of Computing andNational Cheng Kung University, Taiwan)

Ichiro Hasuo (National Institute of Informatics, Japan)

Naohiko Hoshino (Sojo University, Japan)

Guilhem Jaber (Unversite de Nantes, France)

Naoki Kobayashi (University of Tokyo, Japan)

James Laird (University of Bath, UK)

Andrzej Murawski (University of Oxford, UK)

Koko Muroya (RIMS, Kyoto University, Japan)

Ken Sakayori (University of Tokyo, Japan)

Davide Sangiorgi (University Bologna and INRIA, Italy)

Thomas Seiller (CNRS, Université Paris 13, France)

Peter Selinger (Dalhousie University, Canada)

Gabriele Vanoni (IRIF, Université Paris Cité, France)

Glynn Winskel (University of Strathclyde, UK)

Akihisa Yamada (National Institute of Advanced Industrial Science and Technology, Japan)

Nobuko Yoshida (University of Oxford, UK)

Meeting Overview

On the State-of-the-Art

One of the reasons making Girard’s Linear Logic a breakthrough not only in proof theory but also in programming language semantics, is that it enables an interactive view of computation through Game Semantics (GS in the following) and the Geometry of Interaction (GoI in the following). This way, programs are seen as mathematical objects with a rich interactive behaviour (composition in the former, execution in the latter). The two frameworks have been successfully applied to a variety of programming idioms, including those featuring concurrency, various forms of algebraic and quantum effects, etc. In many cases, GS has been proved to characterise observational equivalence through so-called full-abstraction results.

Among the outfalls of GS, one can certainly cite decidability of higher-order model checking, which was initially proved by tools inspired from it, while GoI has been applied to the design of hardware compilation schemes, leading to the so-called Geometry of Synthesis. In either settings, one can describe the dynamics of the interaction between programs and their environ-ments in several ways. In GS, this can take a categorical form, or the operational form of an abstract machine. In GoI, similarly, interaction can be described via traced monoidal categories, operator algebras, or more operationally as an algebra of clauses or as token machine. Different presentations suit different aims.

Current Challenges in Interactive Semantics

Nowadays, Game Semantics and the Geometry of Interaction are very active and lively research fields. Recently, threads of study which have proved to be worthwile being studied in interactive semantics are, e.g.:

• Concurrency. Both in GS and in GoI, capturing some form of parallel or inter-active behaviour have been proved to be challenging but rewarding, leading to denotational models for languages with various forms of concurrent primitives.

• Probabilistic and Quantum Effects. Probabilistic choice from continuous distributions, conditioning, and quantum stores are effects which cannot be modeled by mere function symbols in the style of algebraic effects, and which thus require new ideas to be captured in usual interactive constructions like GS and GoI. Some new results have been recently appeared in the literature, but an overall picture is definitely not there, yet.
  Geometry of Interaction and Efficiency. A series of works have showed that Geometry of Interaction can be seen as a way to interpret higher-order programs in such a way as to be (to a certain extent) space-efficient, at the price of being time-inefficient: the same computation needs to be performed multiple times. There is however an implicit tradeoff to be explored, in which one mixes geometrical and rewriting-based computation mechanisms.

• GS vs. GoI. Game semantics and the Geometry of Interaction are well-known to be closely related, but there are some differences between them, e.g. GoI is a model of linear logic only if a restricted form of reduction relation is considered. Clarifying the relations between the two paradigms would very much help to transfer results between them.

Why a Shonan Meeting?

The research communities on GS and GoI gather together at GaLoP, an annual thematic work-shop on interactive semantics which has been active since 2005, and which is an invaluable occasion for researchers to present their results. Game Semantics has also been the topic of a Daghstuhl Seminar, which one of the three organisers attended, and which proved to be an invaluable occasion not only for presenting results, but also for discussing about ongoing work.

Of the three items mentioned in Section 2 are the subject of a joint project between INRIA and JSPS, called CRECOGI, which is however a relatively small-scale bilateral project between some research labs in France and Japan. More generally, although research on interactive semantics is currently carried out in several countries in Europe, North America and Asia, there is no international joint research project going on, and as a consequence, it is relatively difficult for researchers in the area to exchange ideas in front of a blackboard, at length, and without haste.

We thus believe it is time for the community in interactive semantics to meet for a relatively long period of time, much more than the two days GaLoP typically consists of: new ideas very often comes out of informal discussion between researchers working in very similar projects. For this reason, we plan to structure the meeting around three different forms of presentations:

• Tutorial talks of 60 minutes by experts in nearby areas like probabilistic and quantum computation (we plan to invite at least one expert on both of them, even if not working directly on interactive semantics).

• Short talks about open problems of about 5 to 10 minutes, in which participants can present some challenges they are currently facing in their researches.

• Traditional workshop talks of about 20 to 30 minutes, in which all participants will be given the opportunity to present their recently obtained results.

Towards the end of the meeting, we plan to offer an open space for discussion groups, in which people will interact and discuss about some specific topics of interest. The agenda will be shaped before the meeting, via an online survey between the meeting participants, and there will be parallel sessions. Such a format will be especially interesting to explore advanced research directions and between different but related areas. On advanced topics, we expect to introduce the discussion with a short tutorial, taking advantage of the large spectre of expertise which is guaranteed by the pool of participants. This also will be set before the meeting: in the survey phase, the participants will be able to offer or to demand a talk or a survey on the state-of-the-art of the topics of interest. Demands will be matched with a speaker and allocated in the planning phase.