ISSN 2186-7437

NII Shonan Meeting Report

No. 175

New Directions and Challenges
in Interactive Semantics
Ugo Dal Lago
Claudia Faggian
Naohiko Hoshino
May 20–23, 2024

National Institute of Informatics
2-1-2 Hitotsubashi, Chiyoda-Ku, Tokyo, Japan

New Directions and Challenges
in Interactive Semantics
Organizers:
Ugo Dal Lago (University of Bologna)
Claudia Faggian (CNRS, Université de Paris, France)
Naohiko Hoshino (Sojo University, Japan)
May 20–23, 2024

Background and Introduction
Jean-Yves Girard’s linear logic, introduced in 1987, is a refinement of classicallogic that emphasizes the concept of resource management. Unlike traditional
logical systems, linear logic treats propositions as resources that can be consumed or transformed, rather than being reusable indefinitely. This characteristic makes it particularly suitable for modeling computational processes where
resource usage is a critical concern. In the context of programming language
semantics, linear logic provides a robust framework for reasoning about statechanges, concurrency, and parallelism. It allows for precise control over resource
allocation and deallocation, which is essential for optimizing performance andensuring correctness.
One of the reasons making Girard’s Linear Logic a breakthrough is that it
enables an interactive view of computation through Game Semantics (GS in thefollowing) 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 havebeen successfully applied to a variety of programming idioms, including thosefeaturing concurrency and various forms of effects, etc. In many cases, GS has
been proved to characterize observational equivalence through so-called fullabstraction results.
Among the outfalls of GS, one can certainly cite decidability of higher-ordermodel 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 thedynamics of the interaction between programs and their environments 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 ofclauses or as token machine
Nowadays, Game Semantics and the Geometry of Interaction are active andlively research fields. Recently, threads of study which have proved to be worthwhile being studied in interactive semantics are those related to concurrency,1

in which the interaction can be modeled through causal structures, and that ofprobabilistic and quantum effects. Moreover, Geometry of Interaction can beseen as a way to interpret higher-order programs in such a way as to be (toa certain extent) space-efficient, at the price of being time-inefficient. Finally,
operational game semantics have recently proved to be capable of forming thebasis of automatic tools for equivalence checking of higher-order programs.

Overview of the Meeting
The history of this meeting has been quite troubled. Initially scheduled forspring 2020, it was postponed several times due to the COVID pandemic, which
made it essentially impossible to reach Japan (which for more than two years wasbasically unreachable from the overseas). Only now, four years after the initiallyscheduled date, the workshop was finally held. The number of participants was
24 and is to be considered satisfactory. In addition to a large participation
by Japanese researchers, the participation of researchers from Canada, France,
Italy, Taiwan, UK should also be noted.
The meeting was organized in such a way as to allow all those who wanted
to present their results to do so. In fact, almost all of the participants asked
to give a seminar. While these presentations occupied a significant portion of
the time available, on the other hand, these seminars were the occasion to raise
and identify important topics for discussion, which were then explored in depth
during the breaks, after dinner and on the last day of the workshop.
The atmosphere during the workshop was very cheerful and serene. Everybody’s impression was that all participants were truly interested in the discussions and talks. The excursion to Kamakura, to which almost all the participants
took part, was an opportunity for leisure, but also for informal discussion andexchange of ideas.

Overview of Talks
Linear Algebraic Semantics of Linear Logic
Kazuyuki Asada, Tohoku University, Japan
A number of models of linear logic are based on or closely related to linear
algebra, in the sense that morphisms are “matrices” over appropriate coefficientsets. Examples include models based on coherence spaces, finiteness spaces andprobabilistic coherence spaces, as well as the relational and weighted relationalmodels. This paper introduces a unified framework based on module theory,
making the linear algebraic aspect of the above models more explicit. Specifically we consider modules over Σ-semirings R, which are ring-like structures withpartially-defined countable sums, and show that morphisms in the above models
are actually R-linear maps in the standard algebraic sense for appropriate R.
An advantage of our algebraic treatment is that the category of R-modules islocally presentable, from which it easily follows that this category becomes amodel of intuitionistic linear logic with the cofree exponential. We then discuss
constructions of classical models and show that the above-mentioned models areexamples of our constructions.
2This talk focuses mainly on the work presented at LICS 2022, but includes
some later developments, including the work presented at POPL 2024. This is
joint work with Takeshi Tsukada.

The Many-Worlds Calculus
Kostia Chardonnet, Inria Nancy, France
In this work, we explore the interaction between two monoidal structures:a multiplicative one, for the encoding of pairing, and an additive one, for theencoding of choice. We propose a colored PROP, through a graphical language,
to model computation in this framework where the choice is parameterized byan algebraic side effect: the model can support regular tests, probabilistic andnon-deterministic branching, as well as quantum branching, i.e. superposition.
The language can interpret Multiplicative Additive Linear Logic with units andcan be seen as a graphical representation of (finite dimensional) Weighted Rel. It
comes equipped with two equivalent semantics: a denotational semantics basedon linear applications and a token-based Geometry of Interaction semantics.
Finally, it possesses an equational theory. Through the use of normal forms forthe diagrams, we prove the language to be universal, and the equational theory
to be complete with respect to the semantics.

The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
Pierre Clairambault, CNRS & Aix-Marseille Université, France
Concurrent Games is a framework developed in the past decade for semantics of programming languages. In Concurrent Games, a program is interpreted
as an event structure, representing its interactive behaviour with its execution
environment. The representation is extremely fine-grained: it is causal as inso-called truly concurrent models of concurrency, showing explicitely the dependence and independence of computational events, and the non-deterministic
branching points.
This interpretation is computed in a modular way by induction on programs,
following the methodology of denotational semantics. This is good, because itmeans that the semantics can be used to reason compositionally on programs.
But it is also bad, because the many layers of the interpretation of the sourcecode in a denotational model and the complexity of the operations involved(notably, the composition of strategies) blurs the relationship between the sourcecode and the semantics.
In this work, we make concurrent games operational. More precisely, weshow that programs can be translated compositionally intro certain coloured
Petri nets, combining intuitions from game semantics, Girard’s Geometry ofInteraction, and folklore ideas on the representation of first-order imperative
concurrent programs as Petri nets. We regard these coloured Petri nets as akind of intermediate representation, still close to the source code. But as finite
graphs unfold to infinite trees, Petri nets unfold to event structures; and here weshow that this unfolding yields the same event structure obtained denotationallyfrom the interpretation in concurrent games.
3

We deploy this for Idealized Parallel Algol, a call-by-name higher-order concurrent programming language that is well-studied in the game semantics literature. The translation is implemented, and available at https://ipatopetrinets.
github.io/
This is joint work with Simon Castellan.

Higher-Order Bayesian Networks
Claudia Faggian, CNRS, Université Paris Cité, France
Bayesian networks—a prominent tool for Bayesian reasoning—are graphical first-order probabilistic models. Their strength is to allow for a compact(factorized) representation of large probability distributions, and for efficient inference, both exact and approximate. Their weakness is the lack of modularity
and compositionality.
This talk presents recent work [Faggian Pautasso Vanoni, Popl2024] which
relies on Interactive Semantics to advance along two directions:
1. A first goal, which was already put forward within the Inria-JSPS project
Crecogi, is integrating the efficiency of Bayesian networks with the expressiveness and compositionality of higher-order functional programming.
Ideally, the design of the Bayesian model should be carried at high-level,in the functional language, which allows for recursion and expressive constructs. Higher-order terms then compile (i.e. rewrite) into Bayesian
networks, which serve as the low-level language, and allow for efficient
inference.
2. A second motivation is to advocate cost-awareness in the semantical interpretation, a need that emerged in recent work with Ehrhard and Pagani.
A probabilistic program is a statistical model: to computing its semantics
is to perform inference. Can the semantics be cost-sensitive?
In the talk:• we will present an idealized higher-order probabilistic language, whichallows for the specification of recursive models and hierarchical structures,and prove it sound and complete w.r.t. Bayesian networks: each Bayesian
network can be encoded as a term, and conversely each (possibly higherorder and recursive) program of ground type compiles into a Bayesian
network. The groundwork for the compilation scheme are semantical tools,
based on Geometry of Interaction, rewriting and type systems;• we show that the semantical interpretation of a probabilistic program canbe done at “reasonable” cost , and equip our language with a resourceaware type system, exactly capturing the cost of inference.
This is a joint work with Daniele Pautasso and Gabriele Vanoni, building on
work with Thomas Ehrhard and Michele Pagani.

4

A Modal Linear Logic: its Proof Theory and Semantics
Yosuke Fukuda, Kyoto Tachibana University, JapanThe Curry–Howard correspondence for modal logic has been studied since
the early 90s, and several of these studies are often conducted in relation tometa-programming in the theory of programming languages. However, it is
known that defining the operational semantics of these modal type systems often
becomes more the complex than ordinary type systems, due to the presence of
language features in meta-programming that control programs themselves as
first-class citizens.
Hence, to provide a new perspective on the operational semantics of modal
type systems from the viewpoint of interactive semantics, I’ve been working onreconstructing a modal type system using linear logic. As a first step toward“the operational semantics for modal λ-calculi in a denotational way” (in thesense of interactive semantics), we introduce a linear-logical reconstruction of amodal λ-calculus. In this talk, we will see:
1. A modal linear logic for intuitionistic S4: This logic is introduced
as an extension of MELL (Multiplicative Exponential Linear Logic) witha “bang-box” modality, which is a linear-logical counterpart of the box
modality. This logic can also be seen as a subsystem of subexponential
linear logic or adjoint logic. We show that this logic can encode the boxfragment of intuitionistic modal logic via the modalized Girard translation.
2. The corresponding typed λ-calculus for the modal linear logic:
We then introduce the corresponding typed λ-calculus in the sense of the
Curry–Howard correspondence. We define the calculus as an integration of
the S4 modal λ-calculus of Pfenning and Davies and the dual intuitionistic
linear logic of Barber and Plotkin.
3. (On-going work) An adjoint model of the modal linear λ-calculus:
Since the calculus is given as an integration of a modal calculus and alinear calculus, the semantics of the modal linear λ-calculus is also given
as an integration of the modal-logical model and the linear-logical model.
Technically speaking, the model is defined as a combination of the LNL
model of Benton and the so-called modal category for S4.

Towards Stochastic GoI
Masahiro Hamano, National Cheng Kung University, Taı̈wan
This talk aims to extend my measure theoretic linear exponential models[1, 2] to the Geometry of Interaction (GoI). The primary focus is on transition
kernels between measurable spaces and their convolutional composition. Thisapproach represents a stochastic extension of Rel, capable of incorporating bothstochastic and weighted Rels. Two directions towards GoI are discussed:(Sum style GoI) The biproducts of transition kernels provide a traced monoidal
structure and a primitive exponential in terms of omega copies of the biproducts. This approach leads to a GoI situation (Abramsky-Haghverdi-Scott) thatcoincides with Dal Lago-Hoshino’s model for Bayesian programming (’21).
5

(Product Style GoI) Functorial monoidality is ensured by the Fubini-Tonelli
Theorem through s-finiteness of kernels, as recently revisited by Staton (’17).
Exponentiality is achieved using a counting function on measurable spaces (astochastic version of multiset) and on kernels through push-forward measures.
This measure-theoretic construction is demonstrated to be an instance of the
Melliès-Tabareau-Tasson free exponential construction. We explore the construction of a trace structure consistent with the stochastic exponential comonad.
The discussion includes running execution formulas through the exponential
comonad, with termination managed by the Lebesgue monotone convergence
theorem.
References[1] Masahiro Hamano, A Linear Exponential Comonad in s-finite Transition
Kernels and Probabilistic Coherent Spaces, Information and Computation
295(Part B): 105109 (2023)
https://www.sciencedirect.com/science/article/pii/
S0890540123001128[2] Masahiro Hamano, Double Glueing over Free Exponential: with Measure
Theoretic Applications, [arXiv:2107.07726] (2024)
https://arxiv.org/abs/2107.07726

Compositional Probabilistic Model Checking with String
Diagrams of MDPs
Ichiro Hasuo, National Institute of Informatics, Tokyo, Japan
We present a compositional model checking algorithm for Markov decision
processes, in which they are composed in the categorical graphical languageof string diagrams. The algorithm computes optimal expected rewards. Our
theoretical development of the algorithm is supported by category theory, while
what we call decomposition equalities for expected rewards act as a key enabler.
Experimental evaluation demonstrates its performance advantages. The talk isbased on the following paper:
Watanabe, K., Eberhart, C., Asada, K., Hasuo, I. (2023). Compositional
Probabilistic Model Checking with String Diagrams of MDPs. In: Enea, C., Lal,A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer
Science, vol 13966. Springer, Cham.

On Graded Conway Operator
Naohiko Hoshino, Sojo University, JapanThe notion of Conway operator is a categorical axiomatization of fixed point
operators. Based on an observation about a fixed point operator found in semantic study of differential privacy, we introduce a notion of graded Conway
operator as a generalization of Conway operator. Graded Conway operators
are defined on symmetric monoidal categories with graded linear exponential
comonads, which are categorical counterparts of fine-grained resource sensitive

6

type systems. The main technical observation is that we can construct a graded
Conway operator starting from a graded linear exponential comonad gradedby a Conway semiring and a trace operator that satisfies certain uniformity
conditions.

Open Problems about Parametric Polymorphism
Guilhem Jaber, Nantes Université, FranceThis talk aims to present three major open problems related to parametricpolymorphism and contextual equivalence of System F:
1. The computational interpretation of the abstraction process provided byparametric polymorphism. This question has been studied by Sumii and
Pierce [5] by designing a compilation scheme from System F to an untyped
λ-calculus with an idealized cryptographic primitive called sealing. They
conjectured that this compilation scheme is fully abstract. This conjecture
was recently disproven by Devriese, Patrignani & Piessens [2]. We will
see that by enriching either the source language or the target untyped
language, many interesting questions arise.
2. The completeness of Reynold’s relational parametricity with respect toother notions of parametricity. In this direction, Plotkin & Abadi [7], andAbadi, Cardelli & Curien [1] have asked whether Strachey equivalence,
defined as βη-equivalence of terms once the typing information is erased,
implies Reynold equivalence, defined using logical relations. Such a question remains open today. One may also ask how to characterize logical relations for System F defined using admissible relations that are closed onlyby βη-equivalence (rather than contextual equivalence, as in [3], Chapter
48). A counter-example provided by Sumii and reported in [6] shows thatsuch logical relations are not complete w.r.t. contextual equivalence for
System F.
3. The design of fully abstract denotational models for System F. The state of
the art is Laird’s fully abstract game model for System F equipped withmutable references at all types [4]. But in this language, the universal
type ∃Y.∀X.(X → Y ) × (Y → X) is inhabited, and recursion is encodable
using higher-order references. In order to forbid them, one would need
the usual notion of O-visibility from game semantics, but it is not soundfor this model. Designing a refined notion of O-visibility that is sound isa challenging task. It is a first step to studying innocence for this gamemodel.
We will show that the three questions are intimately linked. We will also present
research directions based on operational game semantics and normal-form bisimulations that provide partial answers to these questions.
References[1] Martı́n Abadi, Luca Cardelli, and Pierre-Louis Curien. Formal parametricpolymorphism. In Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 157–170, 1993.
7

[2] Dominique Devriese, Marco Patrignani, and Frank Piessens. Parametricity
versus the universal type. Proceedings of the ACM on Programming Languages, 2(POPL):1–23, 2017.
[3] Robert Harper. Practical foundations for programming languages. Cambridge University Press, 2016.
[4] James Laird. Game semantics for a polymorphic programming language.
Journal of the ACM (JACM), 60(4):1–27, 2013.
[5] Benjamin Pierce and Eijiro Sumii. Relating cryptography and polymorphism. Available from the authors, 2000.
[6] Andrew M Pitts. Typed operational reasoning. Advanced Topics in Typesand Programming Languages, pages 245–289, 2005.
[7] Gordon Plotkin and Martı́n Abadi. A logic for parametric polymorphism. In
International Conference on Typed Lambda Calculi and Applications, pages
361–375. Springer, 1993.

Interaction Semantics for Completely Lazy PCF
Jim Laird, University of Bath, UK
Game semantics gives a syntax-free, intensional and compositional representation of higher-order functions as strategies. More recent work in denotationalsemantics attaches quantitative information to programs, such as the work required to evaluate them. This talk describes such a denotational cost modelof PCF, which captures so-called “complete laziness”: the cost of evaluating a
program is no more than that of partially evaluating some fragment of it, andthen evaluating the result. So, for example, the evaluation of a β-reduction(λx.M ) N should not duplicate any of the work in N , as this could be avoided
by partially evaluating it first.
In this case, a program is evaluated by computing the finite approximants to
its Böhm tree. The cost of computing an approximant is the size of its (minimal
derivation) in a natural semantics. This satisfies a quantitative version of thestability property: the cost of computing an approximant to C[M ] is the costof computing some unique approximant m of M plus the cost of approximating
C[m]. We show that this cost model is reasonable — it gives the cost of semideciding the approximation relation on a register machine up to constant-factor
overhead – by compiling PCF into a term rewriting system based on its gamesemantics, and applying the techniques of graph-rewriting to the result.

On the Expressivity of Linear Recursion Schemes.
Andrzej Murawski, University of Oxford, UK
In the last decade or so, higher-order recursion schemes (HORS) have emerged
as a promising technique for model-checking higher-order programs. I will discuss several results concerning the case when HORS are typed using linear logic(intuitionistic multiplicative additive linear logic, to be precise). It turns outthat such schemes have an automata-theoretic counterpart, namely restricted8

tree-stack automata, which come from linguistics, where they were introduced
to study the so-called multiple context-free languages. This leads to a new perspective on linear HORS and new decidability results. This is joint work with
Pierre Clairambault (deterministic case, MFCS’19), Guanyan Li and Luke Ong(probabilistic case, LICS’22).

Climbing up a Ladder: a New Approach to Contextual
Refinement
Koko Muroya, Kyoto University, Kyoto, Japan
Contextual refinement is a formalisation of an asymmetric comparison between program fragments. It asserts that the observable result of a programfragment can be reproduced by another program fragment in an arbitrary context. Compiler optimisation, for example, can be validated by proving contextual refinement.
One existing approach to proving contextual refinement is to use Abramsky’s applicative bisimilarity. After constructing an applicative bisimulation,
one needs to prove that the applicative bisimulation is a congruence, whichmeans that the applicative bisimulation is preserved by language constructs.
The proof of congruence typically use Howe’s method.
We propose yet another approach that uses a simulation notion. This approach reverses the two steps of Abramsky’s approach. Namely, one first constructs a relation that is closed under language constructs, and then prove thatthe relation is a simulation. Consequently, this approach does not need Howe’s
method.
In this talk we explain how we are “climbing up a ladder” of advanced features using the new approach: namely, divergence, state, nondeterminism, I/O,
and probability. The first steps on the ladder accommodates only divergence.
We introduced a notion of counting simulation, and showed that graphical local reasoning can be used to establish contextual refinement. The next stepon the ladder was to generalise the notion of counting simulation to accommodate nondeterminism and I/O, introducing a generalised simulation notion
dubbed preoder-constrained simulation. Finally, we refined the first steps using
term-rewriting techniques. We observed that the notion of counting simulation
has a striking similarity with the notion of local coherence that can be foundin the term-rewriting literature. By developing critical pair analysis for local
coherence, we managed partial automation of contextual refinement proofs.

Extensional and Non-extensional Functions as Processes
Ken Sakayori, The University of Tokyo, Japan
This talk is about an interactive semantics of the call-by-name pure λcalculus that is represented by processes. Using Internal π, (a subset of the
π-calculus in which all outputs are bound), we refine the celebrated Milner’s encoding of functions as processes. The refined encoding is parametric on certain
abstract components called wires, which corresponds to the copycat strategies
of game semantics. When wires meet certain mild conditions, the encoding always yields a λ-theory. We show that well-known λ-theories—namely, equalities
9

of Böhm trees, Lévy-Longo trees, and Böhm trees with infinite η—are induced
by instantiating three different wires. (The last instance is, to my knowledge,
the first process encoding of λ-calculus that yields an extensional λ-theory.) In
this talk, I would also like to discuss the similarities and differences between thethree wires and the standard copycat strategies. The three wires have different“control flows”: two are sequential but with opposite directions of flow, and theother has a parallel behavior.

Dynamic Computability
Thomas Seiller, CNRS and Université Sorbonne Paris Nord, France
What is a model of computation? What is a program, an algorithm? Whiletheoretical computer science has been founded on computability theory, the latter does not answer these questions. Indeed, it is a mathematical theory of computable functions, and does not account for computation itself. A symptomaticconsequence is the notion of Turing-completeness. This standard (main) equivalence between models of computation is purely extensional: it does only careabout what is computed and not how, blind to complexity aspects and the question of algorithmic completeness. More importantly, the theory of computationis continuously growing further from how actual machines compute.
I will present a proposal for alternative foundations more faithful to computer science practice and interests, which is fully developed in my habilitation
thesis [1]. This mathematisation of computer science is grounded within the theory of dynamical systems, focussing on how computation is performed rather
than only on what is computed. I will argue that it generalises computability theory while still allowing to recover standard results. After presenting thegeneral framework, I will then discuss how each model of computation defines
families of linear realisability models (realisability models for linear logic). Indeed, the corresponding set of programs can be understood as a generalisationof Girard’s geometry of interaction interpretation of proofs, and satisfy somebasic properties allowing to define a typing systems which models at least themultiplicative-additive fragment of linear logic.
Lastly, I will discuss a path for future work suggested by this work: thepossibility to define a computability and complexity theory accounting moreaccurately for current computer systems and specificities of the architecture(caches, branch prediction) impacting the running time of programs.
References[1] Seiller, Thomas (2024). Mathematical Informatics (Habilitation thesis). Université Sorbonne Paris Nord, https://theses.hal.science/
tel-04616661.

Compositional Semantics for the Game of Hex
Peter Selinger, Dalhousie University, Canada
In game semantics, we usually use games to give a compositional semantics
of programs. On the other hand, combinatorial game theory, introduced by

10

Conway, Berlekamp, and Guy in the 1970s, is about giving a compositionalsemantics of games. In this talk, I will describe a compositional semantics forthe game of Hex.

(Almost) Affine Higher-Order Tree Transducers
Gabriele Vanoni, IRIF, CNRS, Université Paris Cité, France
We investigate the tree-to-tree functions computed by affine λ-transducers:
tree automata whose memory consists of an affine λ-term instead of a finite state.
They can be seen as variations on Gallot, Lemay and Salvati’s Linear High-Order
Deterministic Tree Transducers. When the memory is almost purely affine (àla Kanazawa), we show that these machines can be translated to tree-walking
transducers (and with a purely affine memory, we get a reversible tree-walking
transducer). This leads to a proof of an inexpressivity conjecture of Nguyen
and Pradic on implicit automata in an affine λ-calculus. As a corollary of
our construction, we obtain also characterizations of MSOT and MSOT-S, bypreprocessing the input of λ-transducers by MSO relabeling. The key technicaltool in our proofs is the Interaction Abstract Machine (IAM), an operational
avatar of the geometry of interaction semantics of linear logic. We work withad-hoc specializations to (almost) affine λ-terms of a tree-generating version of
the IAM.

Making Concurrency Functional
Glynn Winskel, University of Strathclyde, UKThis talk bridges between two major paradigms in computation, the functional, at basis computation from input to output, and the interactive, where
computation reacts to its environment while underway. Central to any compositional theory of interaction is the dichotomy between a system and its environment. Concurrent games and strategies address the dichotomy in fine detail,very locally, in a distributed fashion, through distinctions between Player moves(events of the system) and Opponent moves (those of the environment). A functional approach has to handle the dichotomy much more ingeniously, throughits blunter distinction between input and output. This has led to a variety offunctional approaches, specialised to particular interactive demands. Throughconcurrent games we can more clearly see what separates and connects thediffering paradigms, and show how:
• to lift functions to strategies; this helps in describing and programming
strategies by functional techniques.
• several paradigms of functional programming and logic arise naturally as
subcategories of concurrent games, including stable domain theory; nondeterministic dataflow; geometry of interaction; the dialectica interpretation;lenses and optics; and their extensions to containers in dependent lenses
and optics.
• to transfer enrichments of strategies (such as to probabilistic, quantum orreal-number computation) to functional cases.
11

The talk will focus on the second and third points above. (Details can befound in the expanded version of my LICS’23 paper at https://arxiv.org/
abs/2202.13910)

A Stream-Processor Semantics for Cryptographic Random
Programs in Isabelle/HOL
Akihisa Yamada, AIST, JapanWe are formalizing executable cryptography protocols in Isabelle/HOL, basedon CryptHOL. The standard semantics of random programs, as in CryptHOL,
is to view a program as the distribution of the results. This is however notformally compatible when the execution of random programs must be formalized: two programs with the same distribution can return different results whenapplied on the same random seed. Therefore I propose a semantics of random
programs as stream processors, prove some basic monadic properties, and ongoing challenge towards defining the distribution of results of a given random
program.

Session Types, Linear Logics and ExpressivenessNobuko Yoshida, University of Oxford
I first talk about session types and its relationship with expressiveness.
The first technical part of this talk will present an expressiveness result
between Linear Logic-based Session Types and System F. The second part gives
a summary of recent results on session types, highlighting the expressivenesscorrespondence between various session-based process calculi.

List of Participants• Kazuyuki Asada, Tohoky University, Japan• Pierre Clairambault, CNRS, Aix-Marseille Université, France• Kostia Chardonnet, INRIA Nancy, France• Ugo Dal Lago, University of Bologna, Italy• Pietro Di Gianantonio, University of Udine, Italy• Claudia Faggian, CNRS, Université Paris Cité, France• Yosuke Fukuda, Kyoto Tachibana University, Japan• Makoto Hamana, Gunma University, Japan• Masahiro Hamano, School of Computing and National Cheng Kung University, Taı̈wan• Ichiro Hasuo, National Institute of Informatics, Japan• Naohiko Hoshino, Sojo University, Japan12

• Guilhem Jaber, Nantes Université, 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, Université Paris 13, France• Peter Selinger, Dalhousie University, Canada• Gabriele Vanoni, IRIF, Université Paris Cité, France• Glynn Winskel, University of Strathclyde, UK• Akihisa Yamada, National Institute of Advanced Industrial Science andTechnology, Japan• Nobuko Yoshida, University of Oxford, UK

Meeting Schedule
Check-in Day: May 19 (Sun)• 19:00 – 21:00 Welcome Banquet
Day2: May 20 (Mon)• 8:30 – 9:30 Opening• 9:30 – 10:30 Talks and Discussions• 11:00 – 12:00 Talks and Discussions• 13:30 – 15:30 Talks and Discussions• 16:00 – 18:00 Talks and Discussions
Day1: May 21 (Tue)• 9:00 – 10:30 Talks and Discussions• 11:00 – 12:00 Talks and Discussions• 13:30 – 14:00 Group Photo Shooting• 14:00 – 15:30 Talks and Discussions• 16:00 – 18:00 Talks and Discussions
Day3: May 22 (Wed)13• 9:00 – 10:30 Talks and Discussions• 11:00 – 12:00 Talks and Discussions• 13:30 – 21:00 Excursion and Main Banquet
Day4: May 23 (Thu)• 9:00 – 10:30 Talks and Discussions• 11:00 – 12:00 Open discussion

Summary of Discussions and Findings
With participants presenting cutting-edge findings and theoretical advancements, the Meeting fostered a vibrant and diverse discussion. The collaborative
atmosphere encouraged attendees to share insights, tackle open problems, andexplore potential future research directions in interactive semantics. The participants engaged in rich and varied exchanges, that highlighted the interplay
between theoretical foundations and practical applications within programming
languages and computational frameworks, covering a broad range of topics. Below, we list some of these themes, without intending to be exhaustive, but rather
to emphasize some key points of interest.
The Meeting also provided space for smaller group discussions to address
open questions, such as the relevance of higher-order computation to a broader
audience, the quest for a mathematical characterization of interactive semantics, or the development of a notion of observational equivalence that is bothinteractive and quantitative.
Through these multifaceted discussions, the meeting not only highlighted
the current state of research but also paved the way for future investigations
and collaborations in the field.
1. Algebraic and Geometric Approaches to Semantics. Exploring
the integration of algebraic structures, particularly linear algebra, withgeometric interpretations in interactive semantics.
2. Compositionality in Markov Decision Processes. Focus on developing compositional methods for verifying Markov decision processes andtheir applications in probabilistic systems.
3. Probabilistic Programming and Bayesian Reasoning. Discussions
on integrating the expressivity and compositionality of higher-order probabilistic programming with the efficiency of specialized formalisms forBayesian inference, such as graphical models
4. Expressiveness in Higher-Order Recursion Schemes. Exploring
expressiveness and decidability in higher-order recursion schemes, particularly in relation to linear logic and automata-theoretic perspectives.
5. Modal Logic and Higher-Order Types. Investigating the complexities and operational semantics of modal logics and their connection tohigher-order types in programming languages.

14

6. Game Semantics and Concurrency. Examining game semantics asa framework for modeling interactive computations, particularly in thecontext of concurrency and process behaviors.
7. Contextual Refinement and Program Verification. Addressing
methodologies for contextual refinement and the challenges associatedwith proving equivalences in program transformations.
8. Interaction of Categorical Models and Fixed-Point Operators.
Discussing the definitions and applications of fixed-point operators within
categorical frameworks and their implications on resource sensitivity.
9. Relationships between pi-calculi and categorical semantics ofprogramming languages. How a suitably linearly typed π-calculus
can be organized as a categorical model of intuitionistic linear logic, sothat the usual translations of the lambda-calculus arise as instances of thestandard denotational interpretation into a categorical model.
Several other questions have been touched in small groups discussions, suchas those listed below• Why and how is higher-order computation relevant to a wider audience?
• Can we provide a mathematical characterization of what is interactive
semantics?
• How can we develop a notion of observational equivalence which is interactive and quantitative?
• What is the interplay between machine learning (Bayesian learning, Deeplearning) and interactive semantics? How may one be relevant to theother?
• How the following two notions of dependencies relate? On the one hand,the dependencies expressed by concurrent games and event structures, on
the other hand, the dependencies between random variables, for example
those quantified by Pearl’s Bayesian networks.
• Is there a way to turn the KAM Krivin’s machine into a reversible machine,
while preserving (somehow) its time complexity?
• What is the state-of-the-art about expressing Call-by-Value computational
mechanisms by means of Games and Geometry of Interaction? How theseways relate? Can we understand them in a uniform way?

Summary of Identified Issues and Challenges
The Meeting provided a valuable platform for identifying critical issues andchallenges, both in the theoretical foundations and in practical applications. The
discussions underscored several key areas for future exploration and research,
particularly the development of robust methodologies that effectively balance
efficiency and compositionality.

15

Challenges have been emphasized in several areas, spanning from the scalability of verification methods for complex applications, particularly in areas
like concurrency or stochastic processes, to the need for alternative theoreticalfoundations in computation that more accurately represent how actual machinescompute. The discussions highlighted the challenges surrounding contextual
equivalence and parametric polymorphism, along with the integration of various semantic approaches, the necessity for resource-awareness in the semantics
of probabilistic programming, the intricacies of operational semantics in modal
logic, the gap between functional and interactive paradigms, the demand for improved automation in contextual refinement proofs, and several other aspects.
Key issues and challenges highlighted during the Meeting are as follows:
1. Scalability of Verification Methods. Current verification techniques struggle to scale effectively to complex applications involving games, concurrency, and stochastic processes, due to underlying computational costs
and theoretical limitations.
2. Need for alternative foundations in the theory of computation that moreaccurately reflect actual computing practices. A limit of traditional computability theory is to focus primarily on what is computed rather thanhow computation is performed. A need emerges for a framework groundedin dynamical systems and models of computation that can better accountfor architectural specifics, such as caching and branch prediction, influencing program execution time.
3. Challenges in Contextual Equivalence and Parametric Polymorphism. Three
major open problems related to parametric polymorphism and contextual
equivalence of System F:• Understanding the computational interpretation of the abstraction
process provided by parametric polymorphism.
• Investigating whether Strachey equivalence implies Reynold equivalence remains an open question, crucial for understanding parametricity in System F.
• Creating sound and fully abstract denotational models for System
F that accommodate issues like inhabited types and the notion ofO-visibility.
4. Complexity of Operational Semantics in Modal Logic. The operationalsemantics of modal type systems often become more complex than thoseof ordinary type systems due to language features that treat programs as
first-class entities. New perspective brought by interactive semantics andlinear logic.
5. Dichotomy Between Functional and Interactive Paradigms. Bridging the
gap between functional programming and interactive semantics represents
a significant challenge, especially in modeling how systems react to theirenvironments during computation.
6. Automating Contextual Refinement Proofs. There is a need for more efficient ways to automate the proof of contextual refinement, which often

16requires addressing advanced programming features such as state and nondeterminism.
7. Fixed Point Operator Definitions. Issues arise in defining fixed-point operators categorically, especially concerning uniformity conditions requiredfor constructing such operators in resource-sensitive contexts.
8. Integration of Game Semantics and Combinatorial Game Theory. The
challenge of integrating insights from combinatorial game theory withgame semantics remains an area of ongoing development, reflecting a needfor a coherent framework that encompasses both fields.
9. Stochastic Models and Execution Semantics. The development of appropriate execution semantics for stochastic programming, particularly in thecontext of Geometry of Interaction, highlights a need for robust methodologies that account for probabilistic behaviors.
10. Need for Resource-Aware Semantics and Trade-off between Efficiency andCompositionality in probabilistic models. Efficiency and Compositionality
are both crucial issues in probabilistic reasoning, but so far are have beentreated separately. Prominent models such as Bayesian networks allows for
efficient inference, but lack expressivity, modularity and compositionality.
On the other side, the semantics of higher-order probabilistic programming
languages has been focussing on compositionality only. This raise thequest for resource-awareness in the semantical interpretation, particularly
regarding inference.

Takeaways and Future Directions
Interactive semantics is a framework which appears to have the right granularity to effectively bridge high-level mathematical abstraction with the practicalneed to analyze the interactions among various components of a system, facilitating insights into operational behavior and quantitative properties. This
framework appears particularly relevant for addressing emerging needs in software development while simultaneously providing robust theoretical foundations. Examples of areas where this approach is expected to play a crucial role
include higher-order model checking, quantitative reasoning and efficient analysis of performance metrics and resource utilization, probabilistic and quantum
programming languages, compositional analysis and certification of reactive or
effectful programs.
The talks and discussions at the Meeting clearly show that the impact of thetools and methodologies developed within interactive semantics extend beyond
program semantics, into fields such as automata theory, logic, complexity theory,and higher-order model checking.
An important takeaway from the Meeting is the expressed desire for a coordinated international effort to collectively pursue these research directions in a
structured manner. The rich interactions among participants and the progress
made during the workshop indicate a critical mass for initiating a long-term
collaborative project. To foster the collaboration between Europe and Japan onthese topics, we plan in the short term to apply for the Science and Technology
Cooperation Program Sakura, and for the longer term, to apply for a Marie17

Curie Staff Exchange, including partners from Europe and Japan. As a direct
outcome of these findings, preparations are underway also for a research project
proposal on Interactive Semantics to be submitted to the National Research
Agency in France, which will also involve several European and international
partners. This collaborative initiative aims to further advance the research andaddress collectively the challenges and opportunities which have been identified
during the Meeting.

18