A small step towards an Open Source Logic, Investigating models of computation for Linear Realisability
Date(s) : 06/11/2025 iCal
10h00 - 13h00
Jury
Paul-André MELLIES — Rapporteur
Directeur de Recherche
Université Paris-Cité/CNRS
Shin-Ya KATSUMATA — Rapporteur
Full time Professor
Kyoto Sangyo University
Samuel MIMRAM — Président du jury
Professeur des Universités
École Polytechnique
Aurore ALCOLEI — Examinatrice
Maitresse de conférences
Université Paris-Est Créteil Val de Marne (UPEC)
Masahito HASEGAWA — Examinateur
Full Time Professor
Kyoto University
Claudia FAGGIAN — Examinatrice
Chargée de Recherche
Université Paris-Cité/CNRS
Laurent REGNIER — Directeur de thèse
Professeur des Université
Aix Marseille Université
Thomas SEILLER — co-Directeur de thèse
Chargé de Recherche
Université Paris 13/CNRS
Abstract of the Manuscript
This thesis studies computational models used for realizability for linear logic (as part of Geometry of Interaction):
– A first chapter explains the history of the field, presenting several computational models existing in the literature as well as their connection to linear logic.
– A second chapter studies in detail a specific computational model: Seiller’s interaction graphs. We define a generalization of this model, we show that it is an instance of a new, « low-level » framework to define abstract computational model, in which we prove the key property of associativity of execution. This makes it possible to automatically prove this property, and thus to define a computational model for any instance of the framework. We study another instance of the framework solving a problem that existed in a generalization of interaction graphs (thick graphs). Finally, we explain why the model of flows is too general to be an instance of the framework.
– A third chapter focuses on an « intermediate » model: the star model, defined in Eng’s thesis, which generalizes flows in a combinatorial sense, but remains somehow similar to the framework defined previously. We study a new version of this model, correcting and refining essential definitions and properties, some of which, although present in Eng’s thesis, were problematic.
– The final, highly exploratory chapter, attempts to better understand certain combinatorial and geometric properties of the interaction graph model, drawing inspiration from several areas of mathematics (cobordism, directed spaces, category theory…). We also defend the idea that « static locations » are similar to gluing and to the notion of « open system ».
Emplacement
I2M Luminy - TPR2, Amphithéâtre Herbrand 130-134 (1er étage)
Catégories
