7 Mars - 13 Mars


Retour à la vue des calendrier
Vendredi 11 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Interaction Graphs and Quantitative Semantics
Description: Thomas Seiller Interaction Graphs (IG) models were introduced as a generalisation of Girard’s Geometry of Interaction (GOI) constructions based on the interpretation of proofs as (finite, weigthed) graphs. Recent results use IG models to bring into vision a new relation between dynamic and denotational semantics.
The first contribution of this work is the definition of categories of triskells, which generalises both the bicategory of spans and the categories of matrices and arrays over a semiring (also known as categories of weighted relations). Secondly, it sheds light onto a new relationship between dynamic and quantitative denotational semantics for multiplicative linear logic (MLL), providing formal grounds to the claim that IG models are a quantitative generalisation of dynamic semantics, i.e. GOI and game semantics. Finally, this functor is shown to preserve not only the interpretation of proofs but also induced double-glueing refinements: it is shown to lift to a map from the double-glueing construction defining IG models to the double-glueing construction yielding coherence spaces. For this purpose, a very general notion of quantitative coherence spaces is introduced, and shown to model full linear logic.