Document Open Access Logo

Type Isomorphisms for Multiplicative-Additive Linear Logic

Authors Rémi Di Guardia, Olivier Laurent

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.26.pdf
  • Filesize: 0.76 MB
  • 21 pages

Document Identifiers

Author Details

Rémi Di Guardia
  • Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France
Olivier Laurent
  • Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France

Funding

This work was performed within the framework of the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007), and supported by the projects DyVerSe (ANR-19-CE48-0010), QuaReMe (ANR-20-CE48-0005) and ReCiProg (ANR-21-CE48-0019), all operated by the French National Research Agency (ANR). This work was also supported by the IRN Linear Logic.

Cite As Get BibTex

Rémi Di Guardia and Olivier Laurent. Type Isomorphisms for Multiplicative-Additive Linear Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 26:1-26:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSCD.2023.26

Abstract

We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for ⋆-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo [Vincent Balat and Roberto Di Cosmo, 1999]. This yields a much richer equational theory involving distributivity and annihilation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek [Dominic Hughes and Rob van Glabbeek, 2005]. We then use the sequent calculus to extend our results to full MALL (including all units).

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
Keywords
  • Linear Logic
  • Type Isomorphisms
  • Multiplicative-Additive fragment
  • Proof nets
  • Sequent calculus
  • Star-autonomous categories with finite products

Metrics

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

Related Versions

References

  1. Michele Abrusci and Elena Maringelli. A new correctness criterion for cyclic proof nets. Journal of Logic, Language and Information, 7:449-459, 1998. URL: https://doi.org/10.1023/A:1008354130493.
  2. Vincent Balat and Roberto Di Cosmo. A linear logical view of linear type isomorphisms. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 250-265. Springer, 1999. Google Scholar
  3. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181-203, 1989. Google Scholar
  4. Roberto Di Cosmo. Isomorphisms of Types. Progress in Theoretical Computer Science. Birkhäuser, 1995. Google Scholar
  5. Paolo Di Giamberardino. Jump from parallel to sequential proofs: Additives, 2011. URL: https://hal.science/hal-00616386.
  6. Marcelo Fiore, Roberto Di Cosmo, and Vincent Balat. Remarks on isomorphisms in typed lambda calculi with empty and sum types. In Proceedings of the seventeenth annual symposium on Logic In Computer Science, pages 147-156, Copenhagen, July 2002. IEEE, IEEE Computer Society Press. Google Scholar
  7. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  8. Jean-Yves Girard. Proof-nets: the parallel syntax for proof-theory. In Aldo Ursini and Paolo Agliano, editors, Logic and Algebra, volume 180 of Lecture Notes In Pure and Applied Mathematics, pages 97-124, New York, 1996. Marcel Dekker. URL: https://doi.org/10.1201/9780203748671-4.
  9. Willem Heijltjes and Dominic Hughes. Conflict nets: Efficient locally canonical MALL proof nets. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 437-446. ACM Press, July 2016. URL: https://doi.org/10.1145/2933575.2934559.
  10. Dominic Hughes and Rob van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic. ACM Transactions on Computational Logic, 6(4):784-842, 2005. URL: https://doi.org/10.1145/1094622.1094629.
  11. Dominic Hughes and Rob van Glabbeek. MALL proof nets identify proofs modulo rule commutation, 2016. URL: https://arxiv.org/abs/1609.04693.
  12. Olivier Laurent. Classical isomorphisms of types. Mathematical Structures in Computer Science, 15(5):969-1004, October 2005. Google Scholar
  13. Laurent Regnier and Pawel Urzyczyn. Retractions of types with many atoms, 2002. URL: http://arxiv.org/abs/cs/0212005.
  14. Mikael Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1):71-89, 1991. Google Scholar
  15. Robert Seely. Linear logic, ⋆-autonomous categories and cofree coalgebras. Contemporary mathematics, 92, 1989. Google Scholar
  16. Sergei Soloviev. The category of finite sets and cartesian closed categories. Journal of Soviet Mathematics, 22(3):1387-1400, 1983. 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