Glueability of resource proof-structures: inverting the Taylor expansion

Giulio Guerrieri; Luc Pellissier; Lorenzo Tortora de Falco

doi:10.4230/LIPIcs.CSL.2020.24

Glueability of resource proof-structures: inverting the Taylor expansion

Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco

Department of Computer Science

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

3 Citations (SciVal)

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 language	English
Title of host publication	28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain
Editors	Maribel Fernandez, Anca Muscholl
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Chapter	24
Pages	24:1–24:18
Number of pages	18
Volume	152
ISBN (Electronic)	9783959771320
DOIs	https://doi.org/10.4230/LIPIcs.CSL.2020.24
Publication status	Published - 2020

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	152
ISSN (Print)	1868-8969

Keywords

Linear logic
Natural transformation
Proof-net
Taylor expansion

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.CSL.2020.24Licence: CC BY

Cite this

Guerrieri, G., Pellissier, L., & Tortora de Falco, L. (2020). Glueability 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). Article 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

Glueability of resource proof-structures: inverting the Taylor expansion. / Guerrieri, Giulio; Pellissier, Luc; Tortora de Falco, Lorenzo.
28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain. ed. / Maribel Fernandez; Anca Muscholl. Vol. 152 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2020. p. 24:1–24:18 24 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 152).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Guerrieri, G, Pellissier, L & Tortora de Falco, L 2020, Glueability 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, 24, Leibniz International Proceedings in Informatics, LIPIcs, vol. 152, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 24:1–24:18. https://doi.org/10.4230/LIPIcs.CSL.2020.24

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

Guerrieri, Giulio ; Pellissier, Luc ; Tortora de Falco, Lorenzo. / Glueability of resource proof-structures: inverting the Taylor expansion. 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain. editor / Maribel Fernandez ; Anca Muscholl. Vol. 152 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2020. pp. 24:1–24:18 (Leibniz International Proceedings in Informatics, LIPIcs).

@inproceedings{102b3d9c02594ab08b38bcff972738f7,

title = "Glueability of resource proof-structures: inverting the Taylor expansion",

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.",

keywords = "Linear logic, Natural transformation, Proof-net, Taylor expansion",

author = "Giulio Guerrieri and Luc Pellissier and {Tortora de Falco}, Lorenzo",

year = "2020",

doi = "10.4230/LIPIcs.CSL.2020.24",

language = "English",

volume = "152",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

pages = "24:1–24:18",

editor = "Maribel Fernandez and Anca Muscholl",

booktitle = "28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain",

address = "Germany",

}

TY - GEN

T1 - Glueability of resource proof-structures: inverting the Taylor expansion

AU - Guerrieri, Giulio

AU - Pellissier, Luc

AU - Tortora de Falco, Lorenzo

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

KW - Linear logic

KW - Natural transformation

KW - Proof-net

KW - Taylor expansion

UR - http://www.scopus.com/inward/record.url?scp=85078000195&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CSL.2020.24

DO - 10.4230/LIPIcs.CSL.2020.24

M3 - Chapter in a published conference proceeding

VL - 152

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 24:1–24:18

BT - 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain

A2 - Fernandez, Maribel

A2 - Muscholl, Anca

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

ER -

Glueability of resource proof-structures: inverting the Taylor expansion

Abstract

Publication series

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Typed Lambda-Calculi with Sharing and Unsharing

Cite this

Glueability of resource proof-structures: inverting the Taylor expansion

Abstract

Publication series

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Cite this