Interaction Graphs: Exponentials
Logic in Computer Science
2023-06-22 v5 Logic
Abstract
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.
Keywords
Cite
@article{arxiv.1312.1094,
title = {Interaction Graphs: Exponentials},
author = {Thomas Seiller},
journal= {arXiv preprint arXiv:1312.1094},
year = {2023}
}