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 | |
| 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 | Portugal |
| City | Porto |
| Period | 22/06/16 → 26/06/16 |
Keywords
- (differential) linear logic
- Proof-nets
- Relational model
- Taylor expansion
ASJC Scopus subject areas
- Software
Cite this
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 in Book/Report/Conference proceeding › Conference contribution
}
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 - Conference contribution
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
ER -