paperbot · PL 论文追踪

RSS

Interaction Graphs: Exponentials

LMCS vol.Volume 15, Issue 32019
Thomas Seiller

尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。

原文摘要(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.

链接与引用

DOI 原文 ·

BibTeX
@article{paperbot760,
  title = {Interaction Graphs: Exponentials},
  author = {Thomas Seiller},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 3},
  year = {2019},
  doi = {10.23638/lmcs-15(3:25)2019}
}