Thomas Seiller (LAMA - Université de Savoie), Interaction Graphs

Schedule

Abstract

Geometry of Interaction (GoI) is a kind of semantics of linear logic proofs that aims at accounting for the dynamical aspects of cut-elimination. We present here a parametrized construction of a GoI for Multiplicative Additive Linear Logic (MALL) in which proofs are represented by families of directed weighted graphs. This construction is founded on a geometrical identity between sets of cycles which generalizes the three-term adjunctions which sustain usual GoI constructions. Moreover we show how one can obtain, for each value of the parameter, a denotational semantics for MALL from this GoI. Finally, we will explain how this setting is related to Girard's various constructions: two particular choices of the parameter respectively give a combinatorial version of the latest GoI in the hyperfinite factor and a refined version of older GoIs. Our construction hence shows how Girard's various constructions relate to each other by unveiling the unique geometrical identity sustaining them.