Document Open Access Logo

The Relational Model Is Injective for Multiplicative Exponential Linear Logic

Author Daniel de Carvalho

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.41.pdf
  • Filesize: 0.83 MB
  • 19 pages

Document Identifiers

Author Details

Daniel de Carvalho

Cite As Get BibTex

Daniel de Carvalho. The Relational Model Is Injective for Multiplicative Exponential Linear Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CSL.2016.41

Abstract

We prove a completeness result for Multiplicative Exponential Linear Logic (MELL): we show that the relational model is injective for MELL proof-nets, i.e. the equality between MELL proof-nets in the relational model is exactly axiomatized by cut-elimination.

Subject Classification

Keywords
  • Linear Logic
  • Denotational semantics
  • Proof-nets

Metrics

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

References

  1. Pierre Boudes. Unifying static and dynamic denotational semantics. Technical report, Institut de Mathématiques de Luminy, 2004. Google Scholar
  2. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. The inhabitation problem for non-idempotent intersection types. In Josep Diaz, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, volume 8705 of Lecture Notes in Computer Science, pages 341-354. Springer, 2014. Google Scholar
  3. Vincent Danos. La Logique Linéaire appliquée à l'étude de divers processus de normalisation. Ph.D. thesis, Université Paris 7, 1990. Google Scholar
  4. Vincent Danos and Laurent Regnier. Proof-nets and the Hilbert space. In Advances in Linear Logic, volume 222 of London Math. Soc. Lecture Note Ser. Cambridge University Press, 1995. Google Scholar
  5. René David and Walter Py. λμ-calculus and Böhm’s theorem. Journal of Symbolic Logic, 66(1):407-413, March 2001. Google Scholar
  6. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. Ph.D. thesis, Université Aix-Marseille II, 2007. Google Scholar
  7. Daniel de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. RR 6638, INRIA, 2008. To appear in Mathematical Structures in Computer Science. Google Scholar
  8. Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. A semantic measure of the execution time in linear logic. Theoretical Computer Science, 412/20:1884-1902, 2011. Google Scholar
  9. Daniel de Carvalho and Lorenzo Tortora de Falco. The relational model is injective for multiplicative exponential linear logic (without weakenings). Annals of Pure and Applied Logic, 163(9):1210-1236, 2012. Google Scholar
  10. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Theoretical Computer Science, 364:166-195, 2006. Google Scholar
  11. Harvey Friedman. Equality between functionals. Lecture Notes in Mathematics, 453, 1975. Google Scholar
  12. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  13. Giulio Guerrieri, Lorenzo Tortora De Falco, and Luc Pellissier. Injectivity of relational semantics for (connected) mell proof-nets via taylor expansion, 2014. URL: https://hal.archives-ouvertes.fr/hal-00998847.
  14. Willem Heijltjes and Robin Houston. No proof nets for MLL with units: proof equivalence in MLL is pspace-complete. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS'14, Vienna, Austria, July 14-18, 2014, pages 50:1-50:10. Association for Computing Machinery, 2014. Google Scholar
  15. Dominic J. D. Hughes and Rob J. van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic (extended abstract). In Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003), pages 1-10. IEEE Computer Society Press, 2003. Google Scholar
  16. Gianfranco Mascari and Marco Pedicini. Head linear reduction and pure proof net extraction. Theor. Comput. Sci., 135(1), 1994. Google Scholar
  17. Satoshi Matsuoka. Weak typed böhm theorem on imll. Annals of Pure and Applied Logic, 145(1):37-90, 2007. Google Scholar
  18. Damiano Mazza and Michele Pagani. The separation theorem for differential interaction nets. In Proceedings of the 14th LPAR International Conference, volume 4790 of LNAI. Springer, 2007. Google Scholar
  19. Michele Pagani. Proofs, denotational semantics and observational equivalences in multiplicative linear logic. Mathematical Structures in Computer Science, 17(2):341-359, 2007. URL: http://dx.doi.org/10.1017/S0960129506005652.
  20. Michele Pagani and Christine Tasson. The taylor expansion inverse problem in linear logic. In Proceedings of the 24th ANNUAL IEEE Symposium on Logic in Computer Science, 2009. Google Scholar
  21. Simona Ronchi Della Rocca. Principal type scheme and unification for intersection type discipline. Theoretical Computer Science, 59:181-209, 1988. Google Scholar
  22. Alexis Saurin. Separation with streams in the lambda-mu-calculus. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, 2005. Google Scholar
  23. Lorenzo Tortora de Falco. Réseaux, cohérence et expériences obsessionnelles. Ph.D. thesis, Université Paris 7, January 2000. Google Scholar
  24. Lorenzo Tortora de Falco. Obsessional experiments for linear logic proof-nets. Mathematical Structures in Computer Science, 13(6):799-855, 2003. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact