Published in

Logical Methods in Computer Science ; Volume 15, p. Issue 3 ; 1860-5974, 2019

DOI: 10.23638/lmcs-15(3:25)2019

Links

Tools

Export citation

Search in Google Scholar

Interaction Graphs: Exponentials

Journal article published in 2013 by Thomas Seiller ORCID
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Question mark in circle
Preprint: policy unknown
Question mark in circle
Postprint: policy unknown
Question mark in circle
Published version: policy unknown

Abstract

This paper is the fourth of a series exposing a systematic combinatorial approach to Girard's Geometry of Interaction program. This program aims at obtaining particular realizability 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. In order to succeed in this, we use the notion of graphings, a generalization of graphs which was defined in earlier work. We explain how we can use this framework 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.