Thomas Seiller - Interaction Graphs: Exponentials

lmcs:5712 - Logical Methods in Computer Science, August 30, 2019, Volume 15, Issue 3 - https://doi.org/10.23638/LMCS-15(3:25)2019
Interaction Graphs: ExponentialsArticle

Authors: Thomas Seiller ORCID

    This paper is the fourth of a series exposing a systematic combinatorial approach to Girard's Geometry of Interaction (GoI) program. The GoI program aims at obtaining particular realisability models for linear logic that accounts for the dynamics of cut-elimination. This fourth paper tackles the complex issue of defining exponential connectives in this framework. For that purpose, we use the notion of \emph{graphings}, a generalisation of graphs which was defined in earlier work. We explain how to define a GoI for Elementary Linear Logic (ELL) with second-order quantification, a sub-system of linear logic that captures the class of elementary time computable functions.


    Volume: Volume 15, Issue 3
    Published on: August 30, 2019
    Accepted on: August 26, 2019
    Submitted on: August 26, 2019
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,03B70, 03F52, 28E15,F.3.2,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Logic and Geometry of Interaction; Funder: French National Research Agency (ANR); Code: ANR-10-BLAN-0213
    • A Realizability Approach to Complexity Theory; Funder: European Commission; Code: 659920

    Consultation statistics

    This page has been seen 1517 times.
    This article's PDF has been downloaded 338 times.