Interaction Graphs: Exponentials

MaRDI QIDQ6246993arXivFDO

Authors Thomas Seiller

Publication date 4 December 2013

Published in arXiv

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Semantics in the theory of computing (68Q55)

arXiv classification

cs.LOmath.LO

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.

This page was built for publication: Interaction Graphs: Exponentials

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6246993)