Computing connected proof(-Structure)s from their taylor expansion

Giulio Guerrieri; Luc Pellissier; Lorenzo Tortora De Falco

doi:10.4230/LIPIcs.FSCD.2016.20

Computing connected proof(-Structure)s from their 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

15 Citations (SciVal)

Abstract

We show that every connected Multiplicative Exponential Linear Logic (MELL) proof-structure (with or without cuts) is uniquely determined by a well-chosen element of its Taylor expansion: the one obtained by taking two copies of the content of each box. As a consequence, the relational model is injective with respect to connected MELL proof-structures.

Original language	English
Title of host publication	1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
Editors	Delia Kesner, Brigitte Pientka
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume	52
ISBN (Electronic)	9783959770101
DOIs	https://doi.org/10.4230/LIPIcs.FSCD.2016.20
Publication status	Published - 1 Jun 2016
Event	1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal Duration: 22 Jun 2016 → 26 Jun 2016

Publication series

Name	LIPIcs : Leibniz International Proceedings in Informatics
Publisher	Schloss Dagstuhl
ISSN (Print)	1868-8969

Conference

Conference	1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
Country/Territory	Portugal
City	Porto
Period	22/06/16 → 26/06/16

Funding

Thanks to Daniel de Carvalho for pointing out that our approach to prove the injectivity of the relational semantics is not limited to ACC MELL-ps. Proofnets are drawn using (a slight modification of) Marc Bagnol's package pn.sty. This work has been partially supported by the French ANR projects ANR-11-IS02-0002 (Locali) and ANR-12-JS02-0006 (CoQuaS), and the French A?MIDEX project ANR-11-IDEX-0001-02.

Keywords

(differential) linear logic
Proof-nets
Relational model
Taylor expansion

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.FSCD.2016.20Licence: CC BY

Cite this

Guerrieri, G., Pellissier, L., & De Falco, L. T. (2016). Computing connected proof(-Structure)s from their taylor expansion. In D. Kesner, & B. Pientka (Eds.), 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 (Vol. 52). Article 20 (LIPIcs : Leibniz International Proceedings in Informatics). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2016.20

Computing connected proof(-Structure)s from their taylor expansion. / Guerrieri, Giulio; Pellissier, Luc; De Falco, Lorenzo Tortora.
1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. ed. / Delia Kesner; Brigitte Pientka. Vol. 52 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2016. 20 (LIPIcs : Leibniz International Proceedings in Informatics).

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

Guerrieri, G, Pellissier, L & De Falco, LT 2016, Computing connected proof(-Structure)s from their taylor expansion. in D Kesner & B Pientka (eds), 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. vol. 52, 20, LIPIcs : Leibniz International Proceedings in Informatics, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, Porto, Portugal, 22/06/16. https://doi.org/10.4230/LIPIcs.FSCD.2016.20

Guerrieri G, Pellissier L, De Falco LT. Computing connected proof(-Structure)s from their taylor expansion. In Kesner D, Pientka B, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. Vol. 52. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2016. 20. (LIPIcs : Leibniz International Proceedings in Informatics). doi: 10.4230/LIPIcs.FSCD.2016.20

Guerrieri, Giulio ; Pellissier, Luc ; De Falco, Lorenzo Tortora. / Computing connected proof(-Structure)s from their taylor expansion. 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. editor / Delia Kesner ; Brigitte Pientka. Vol. 52 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2016. (LIPIcs : Leibniz International Proceedings in Informatics).

@inproceedings{e18ef93804b241eb83798ff1454dbe41,

title = "Computing connected proof(-Structure)s from their taylor expansion",

abstract = "We show that every connected Multiplicative Exponential Linear Logic (MELL) proof-structure (with or without cuts) is uniquely determined by a well-chosen element of its Taylor expansion: the one obtained by taking two copies of the content of each box. As a consequence, the relational model is injective with respect to connected MELL proof-structures.",

keywords = "(differential) linear logic, Proof-nets, Relational model, Taylor expansion",

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

year = "2016",

month = jun,

day = "1",

doi = "10.4230/LIPIcs.FSCD.2016.20",

language = "English",

volume = "52",

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

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

editor = "Delia Kesner and Brigitte Pientka",

booktitle = "1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016",

address = "Germany",

note = "1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 ; Conference date: 22-06-2016 Through 26-06-2016",

}

TY - GEN

T1 - Computing connected proof(-Structure)s from their taylor expansion

AU - Guerrieri, Giulio

AU - Pellissier, Luc

AU - De Falco, Lorenzo Tortora

PY - 2016/6/1

Y1 - 2016/6/1

N2 - We show that every connected Multiplicative Exponential Linear Logic (MELL) proof-structure (with or without cuts) is uniquely determined by a well-chosen element of its Taylor expansion: the one obtained by taking two copies of the content of each box. As a consequence, the relational model is injective with respect to connected MELL proof-structures.

AB - We show that every connected Multiplicative Exponential Linear Logic (MELL) proof-structure (with or without cuts) is uniquely determined by a well-chosen element of its Taylor expansion: the one obtained by taking two copies of the content of each box. As a consequence, the relational model is injective with respect to connected MELL proof-structures.

KW - (differential) linear logic

KW - Proof-nets

KW - Relational model

KW - Taylor expansion

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

U2 - 10.4230/LIPIcs.FSCD.2016.20

DO - 10.4230/LIPIcs.FSCD.2016.20

M3 - Chapter in a published conference proceeding

AN - SCOPUS:84977547142

VL - 52

T3 - LIPIcs : Leibniz International Proceedings in Informatics

BT - 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016

A2 - Kesner, Delia

A2 - Pientka, Brigitte

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

T2 - 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016

Y2 - 22 June 2016 through 26 June 2016

ER -

Computing connected proof(-Structure)s from their taylor expansion

Abstract

Publication series

Conference

Funding

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this