One of the reasons making Girard’s Linear Logic [14] 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 [2, 18] (GS in the following)and the Geometry of Interaction [15] (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 [21], while GoI has been applied to the design of hardware compilation schemes, leading to the so-called Geometry of Synthesis [13]. 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, as in [7]. In GoI, similarly, interaction can be described via traced monoidal categories [1], operator algebras [17], or more operationally as an algebra of clauses [16, 4] or as token machine [12]. Different presentations suit different aims.

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 [3, 23] and in GoI [8], 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 [22, 20], 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 [9, 6], 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 [10], 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, as hinted in [19].

• GS vs. GoI. Game semantics and the Geometry of Interaction are well-known to be closely related [11, 5], 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.

The research communities on GS and GoI gather together at GaLoP[1], 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[2], 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[3], 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 (see Section 2 above) 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.

[1] http://www.gamesemantics.org/
[2] https://www.dagstuhl.de/10252
[3] More information here: http://crecogi.cs.unibo.it/

[1] Samson Abramsky, Esfandiar Haghverdi, and Philip J. Scott. Geometry of interaction and linear combinatory algebras. Mathematical Structures in Computer Science, 12(5):625–665, 2002.
[2] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409–470, 2000.
[3] Samson Abramsky and Paul-Andre´ Melli`es. Concurrent games and full completeness. In Proc. of LICS 1999, pages 431–442, 1999.
[4] Cl´ement Aubert, Marc Bagnol, Paolo Pistone, and Thomas Seiller. Logic programming and logarithmic space. In Proc. of APLAS, pages 39–57, 2014.
[5] Patrick Baillot. Approches dynamiques en s´emantique de la logique lineaire: jeux et g´eometrie de l’interaction. PhD thesis, Universite Aix-Marseille 2, 1999.
[6] Pierre Clairambault and Hugo Paquet. Fully abstract models of the probabilistic lambda-calculus. In Proc. of CSL, pages 16:1–16:17, 2018.
[7] Pierre-Louis Curien and Hugo Herbelin. Abstract machines for dialogue games. Available at http://arxiv. org/abs/0706.2544, 2007.
[8] Ugo Dal Lago, Claudia Faggian, Benoˆıt Valiron, and Akira Yoshimizu. Parallelism and synchronization in an infinitary context. In Proc. of LICS, pages 559–572, 2015.
[9] Ugo Dal Lago, Claudia Faggian, Benoˆıt Valiron, and Akira Yoshimizu. The geometry of parallelism: classical, probabilistic, and quantum effects. In Proc. of POPL 2017, pages 833–845, 2017.
[10] Ugo Dal Lago and Ulrich Sch¨opp. Computation by interaction for space-bounded functional programming. Inf. Comput., 248:150–194, 2016.
[11] Vincent Danos, Hugo Herbelin, and Laurent Regnier. Game semantics & abstract machines. In Proc. of LICS, pages 394–405, 1996.
[12] Vincent Danos and Laurent Regnier. Reversible, irreversible and optimal lambda-machines. Theor. Comput. Sci., 227(1-2):79–97, 1999.
[13] Dan R. Ghica. Geometry of synthesis: a structured approach to VLSI design. In Proc. of POPL, pages 363–375, 2007.
[14] Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1–102, 1987.
[15] Jean-Yves Girard. Geometry of interaction 1: interpretation of system F. In Proceedings of Logic Colloquium ’88, pages 221–260, 1989.
[16] Jean-Yves Girard. Geometry of interaction III: Accomodating the additives. In Advances in Linear Logic, number 222 in London Mathematical Society Lecture Notes Series. Cambridge University Press, 1995.
[17] Jean-Yves Girard. Geometry of interaction V: Logic in the hyperfinite factor. Theor. Comput. Sci., 412(20):1860–1883, 2011.
[18] J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285–408, 2000.
[19] Koko Muroya and Dan R. Ghica. The dynamic geometry of interaction machine: A call-by-need graph rewriter. In Proc. of CSL, pages 32:1–32:15, 2017.
[20] Koko Muroya, Naohiko Hoshino, and Ichiro Hasuo. Memoryful geometry of interaction II: recursion and adequacy. In Proc. of POPL, pages 748–760, 2016.
[21] C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In Proc. of LICS, pages 81–90, 2006.
[22] Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In Proc. of FOSSACS, pages 1–24, 2001.
[23] Silvain Rideau and Glynn Winskel. Concurrent strategies. In Proc. of LICS 2011, pages 409–418, 2011.