#### Thomas Seiller (INRIA-Université de Savoie, Chambery)

#### Interaction Graphs: the geometry behind Geometry of Interaction

Abstract:
The Interaction Graphs construction gives a unified vision of the
various constructions of GoI defined by Girard, while simplifying them
by replacing operators acting on an infinite-dimensional Hilbert space
with directed weighted graphs. Moreover, it brings to light a
geometrical identity which is the sole property that support the whole
construction of a geometry of interaction (GoI) for multiplicative
additive linear logic (MALL).
I will first define and explain the Interaction Graphs construction.
This construction is founded on the cyclic property, a geometrical
identity satisfied by the sets of cycles that alternate between two
graphs, and is parametrized by the choice of a map that "measures"
cycles. I will explain how to define a GoI for MALL in this setting, and
how to derive a categorical model of multiplicative linear logic,
i.e. a *-autonomous catergory, from it.
The framework of interaction graphs however shares with other GoI
constructions dealing with additives the issue that the connective & do
not define a categorical product in the derived *-autonomous category. I
will explain how this problem can be solved by defining a notion of
observational equivalence, which turns out to be a congruence, and
quotienting the category.
I will then show how these constructions are related to Girard's various
GoI construction: a first value of the parameter defines a slight
refinement of the old GoI constructions (GoI1,GoI2,GoI3), while a second
value defines a combinatorial version of the "geometry of interaction in
the hyperfinite factor" (GoI5).