Computing Connected Proof(-Structure)s From Their Taylor Expansion

Authors Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco

Thumbnail PDF


  • Filesize: 0.82 MB
  • 18 pages

Document Identifiers

Author Details

Giulio Guerrieri
Luc Pellissier
Lorenzo Tortora de Falco

Cite AsGet BibTex

Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Computing Connected Proof(-Structure)s From Their Taylor Expansion. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


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.
  • proof-nets
  • (differential) linear logic
  • relational model
  • Taylor expansion


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical logic, 28(3):181-203, 1989. Google Scholar
  2. V. Danos and L. Regnier. Proof-nets and the Hilbert space. In Advances in Linear Logic, pages 307-328. Cambridge University Press, 1995. Google Scholar
  3. D. de Carvalho. The relational model is injective for Multiplicative Exponential Linear Logic. Preprint available at, April 2015.
  4. D. de Carvalho, M. Pagani, and L. Tortora de Falco. A semantic measure of the execution time in Linear Logic. Theoretical Computer Science, 412(20):1884-1902, 2011. Google Scholar
  5. D. de Carvalho and L. Tortora de Falco. The relational model is injective for multiplicative exponential linear logic (without weakening). Ann. Pure Appl. Logic, 163(9):1210-1236, 2012. Google Scholar
  6. T. Ehrhard. Finiteness spaces. Math. Struct. Comp. Science, 15(4):615-646, 2005. Google Scholar
  7. T. Ehrhard and L. Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1-3):1-41, 2003. Google Scholar
  8. T. Ehrhard and L. Regnier. Differential interaction nets. Theoretical Computer Science, 364(2):166-195, 2006. Google Scholar
  9. T. Ehrhard and L. Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2-3):347-372, 2008. Google Scholar
  10. H. Friedman. Equality between functionals. In Rohit Parikh, editor, Logic Colloquium, volume 453 of Lecture Notes in Mathematics, pages 22-37. Springer Berlin, 1975. Google Scholar
  11. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987. Google Scholar
  12. G. Guerrieri, L. Pellissier, and L. Tortora de Falco. Syntax, Taylor expansion and relational semantics of MELL proof-structures: an unusual approach. Technical report, 2016. Available at URL:
  13. Y. Lafont. From Proof-Nets to Interaction Nets. In Advances in Linear Logic, pages 225-247. Cambridge University Press, 1995. Google Scholar
  14. O. Laurent. Polarized proof-nets and λμ-calculus. Theor. Comp. Sci., 290(1):161-188, 2003. Google Scholar
  15. D. Mazza and M. Pagani. The Separation Theorem for Differential Interaction Nets. In Proceedings of LPAR 2007, pages 393-407, 2007. Google Scholar
  16. M. Pagani. The Cut-Elimination Thereom for Differential Nets with Boxes. In Proceedings of TLCA 2009, pages 219-233, 2009. Google Scholar
  17. M. Pagani and C. Tasson. The Taylor Expansion Inverse Problem in Linear Logic. In Proceedings of LICS 2009, pages 222-231, 2009. Google Scholar
  18. R. Statman. Completeness, invariance and λ-definability. J. Symb. Logic, 47(1):17-26, 1982. Google Scholar
  19. L. Tortora de Falco. Obsessional Experiments For Linear Logic Proof-Nets. Mathematical Structures in Computer Science, 13(6):799-855, December 2003. Google Scholar
  20. P. Tranquilli. Intuitionistic differential nets and lambda-calculus. Theoretical Computer Science, 412(20):1979-1997, 2011. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail