Glueability and coherence of resource proof-structures: inverting the Taylor expansion

Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures.

Original languageEnglish
Title of host publication28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain
EditorsMaribel Fernandez, Anca Muscholl
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Chapter24
Pages24:1–24:18
Number of pages18
Volume152
ISBN (Electronic)9783959771320
DOIs
Publication statusPublished - 2020

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume152
ISSN (Print)1868-8969

Keywords

  • Linear logic
  • Natural transformation
  • Proof-net
  • Taylor expansion

ASJC Scopus subject areas

  • Software

Cite this

Guerrieri, G., Pellissier, L., & Tortora de Falco, L. (2020). Glueability and coherence of resource proof-structures: inverting the Taylor expansion. In M. Fernandez, & A. Muscholl (Eds.), 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain (Vol. 152, pp. 24:1–24:18). [24] (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 152). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2020.24