Document Open Access Logo

Linear Realisability over Nets: Multiplicatives

Authors Adrien Ragot , Thomas Seiller , Lorenzo Tortora de Falco

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.43.pdf
  • Filesize: 1.07 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Program semantics
Keywords
  • Linear Logic
  • Proof Nets
  • Realisability
  • Orthogonality
  • Hypergraphs
  • Rewriting
  • Correctness

Metrics

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

Abstract

We provide a new realisability model based on orthogonality for the multiplicative fragment of linear logic, both in presence of generalised axioms (MLL^✠) and in the standard case (MLL). The novelty is the definition of cut elimination for generalised axioms. We prove that our model is adequate and complete both for MLL^✠ and MLL.

Cite As Get BibTex

Adrien Ragot, Thomas Seiller, and Lorenzo Tortora de Falco. Linear Realisability over Nets: Multiplicatives. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 43:1-43:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.43

Author Details

Adrien Ragot
  • LIPN - UMR 7030 CNRS, Université Sorbonne Paris Nord, France
  • Dipartimento di Matematica e Fisica, Università Degli Studi Roma Tre, Italy
Thomas Seiller
  • CNRS, LIPN - UMR 7030, Université Sorbonne Paris Nord, France
Lorenzo Tortora de Falco
  • Dipartimento di Matematica e Fisica, Università Degli Studi Roma Tre, Italy
  • GNSAGA, Istituto Nazionale di Alta Matematica, Roma, Italy

Funding

  • Ragot, Adrien: Supported by a VINCI PhD fellowship from the Franco-Italian Université.
  • Seiller, Thomas: Partially supported by the ANR-22-CE48-0003-01 project DySCo.

References

  1. Denis Bechet. Minimality of the correctness criterion for multiplicative proof nets. Mathematical Structures in Computer Science, 8(6):543-558, 1998. URL: http://journals.cambridge.org/action/displayAbstract?aid=44779, URL: https://doi.org/10.1017/S096012959800262X.
  2. Emmanuel Beffara. A concurrent model for linear logic. Electronic Notes in Theoretical Computer Science, 155:147-168, 2006. Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI). URL: https://doi.org/10.1016/j.entcs.2005.11.055.
  3. Emmanuel Beffara, Félix Castro, Mauricio Guillermo, and Étienne Miquey. Concurrent realizability on conjunctive structures. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 28:1-28:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.FSCD.2023.28.
  4. Pierre-Louis Curien. Introduction to linear logic and ludics, part II. CoRR, abs/cs/0501039, 2005. URL: https://arxiv.org/abs/cs/0501039.
  5. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28(3):181-203, October 1989. URL: https://doi.org/10.1007/BF01622878.
  6. Valeria C. V. de Paiva. A dialectica-like model of linear logic. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, pages 341-356, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFB0018360.
  7. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  8. Jean-Yves Girard. Multiplicatives. In G. Lolli, editor, Logic and Computer Science: New Trends and Applications, pages 11-34. Rosenberg & Sellier, 1987. Google Scholar
  9. Jean-Yves Girard. Proof-nets: The parallel syntax for proof-theory. In Logic and Algebra, pages 97-124. Marcel Dekker, 1996. Google Scholar
  10. Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. In Laurent Fribourg, editor, Computer Science Logic, pages 38-38, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  11. Jean-Baptiste Joinet and Thomas Seiller. From abstraction and indiscernibility to classification and types: revisiting hermann weyl’s theory of ideal elements. Kagaku tetsugaku, 53(2):65-93, 2021. URL: https://doi.org/10.4216/jpssj.53.2_65.
  12. Jean-Louis Krivine. Realizability in classical logic. Panoramas et synthèses, 27:197-229, 2005. URL: https://hal.science/hal-00154500.
  13. International Research Network (IRN) Linear Logic. Handbook of Linear Logic. International Research Network (IRN) Linear Logic, 2023. URL: https://ll-handbook.frama.io/ll-handbook/ll-handbook-public.pdf.
  14. Paulo Oliva. Modified realizability interpretation of classical linear logic. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 431-442, 2007. URL: https://doi.org/10.1109/LICS.2007.32.
  15. Thomas Seiller. Interaction graphs: Multiplicatives. Annals of Pure and Applied Logic, 163(12):1808-1837, 2012. URL: https://doi.org/10.1016/j.apal.2012.04.005.
  16. Thomas Seiller. Interaction graphs: Exponentials. Log. Methods Comput. Sci., 15, 2013. Google Scholar
  17. Thomas Seiller. Interaction graphs: Full linear logic. CoRR, abs/1504.04152, 2015. URL: https://arxiv.org/abs/1504.04152.
  18. Thomas Seiller. Interaction graphs: Additives. Annals of Pure and Applied Logic, 167(2):95-154, 2016. URL: https://doi.org/10.1016/j.apal.2015.10.001.
  19. Thomas Seiller. Interaction graphs: Graphings. Annals of Pure and Applied Logic, 168(2):278-320, 2017. URL: https://doi.org/10.1016/j.apal.2016.10.007.
  20. Thomas Seiller. Mathematical informatics, 2024. Habilitation thesis. URL: https://theses.hal.science/tel-04616661.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact