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

Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora De Falco

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

4 Citations (Scopus)

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 languageEnglish
Title of host publication1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
EditorsDelia Kesner, Brigitte Pientka
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume52
ISBN (Electronic)9783959770101
DOIs
Publication statusPublished - 1 Jun 2016
Event1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal
Duration: 22 Jun 201626 Jun 2016

Publication series

NameLIPIcs : Leibniz International Proceedings in Informatics
PublisherSchloss Dagstuhl
ISSN (Print)1868-8969

Conference

Conference1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
CountryPortugal
CityPorto
Period22/06/1626/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

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 proceedingConference contribution

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). https://doi.org/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 = "6",
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",

}

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 -