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

6 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