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
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). [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