Document Open Access Logo

A Mixed Linear and Graded Logic: Proofs, Terms, and Models

Authors Victoria Vollmer , Danielle Marshall , Harley Eades III , Dominic Orchard

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.32.pdf
  • Filesize: 0.87 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • linear logic
  • graded modal logic
  • adjoint decomposition

Metrics

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

Abstract

Graded modal logics generalise standard modal logics via families of modalities indexed by an algebraic structure whose operations mediate between the different modalities. The graded "of-course" modality !_r captures how many times a proposition is used and has an analogous interpretation to the of-course modality from linear logic; the of-course modality from linear logic can be modelled by a linear exponential comonad and graded of-course can be modelled by a graded linear exponential comonad. Benton showed in his seminal paper on Linear/Non-Linear logic that the of-course modality can be split into two modalities connecting intuitionistic logic with linear logic, forming a symmetric monoidal adjunction. Later, Fujii et al. demonstrated that every graded comonad can be decomposed into an adjunction and a "strict action". We give a similar result to Benton, leveraging Fujii et al.’s decomposition, showing that graded modalities can be split into two modalities connecting a graded logic with a graded linear logic. We propose a sequent calculus, its proof theory and categorical model, and a natural deduction system which we show is isomorphic to the sequent calculus system. Interestingly, our system can also be understood as Linear/Non-Linear logic composed with an action that adds the grading, further illuminating the shared principles between linear logic and a class of graded modal logics.

Cite As Get BibTex

Victoria Vollmer, Danielle Marshall, Harley Eades III, and Dominic Orchard. A Mixed Linear and Graded Logic: Proofs, Terms, and Models. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.32

Author Details

Victoria Vollmer
  • School of Computing, University of Kent, UK
Danielle Marshall
  • School of Computing, University of Kent, UK
Harley Eades III
  • Computer Science, Augusta University, GA, USA
Dominic Orchard
  • School of Computing, University of Kent, UK
  • Department of Computer Science and Technology, University of Cambridge, UK

Funding

This work was supported in part by the EPSRC grant EP/T013516/1 (Verifying Resource-like Data Use in Programs via Types). The second author received support through Schmidt Sciences, LLC.

Acknowledgements

We thank all the anonymous reviewers of this, and previous versions, of this paper. We are also grateful for discussions with Peter Hanukaev and helpful comments from Paulo Torrens on a draft of this manuscript.

References

  1. Andreas Abel and Jean-Philippe Bernardy. A unified view of modalities in type systems. Proc. ACM Program. Lang., 4(ICFP):90:1-90:28, 2020. URL: https://doi.org/10.1145/3408972.
  2. Robert Atkey. Syntax and Semantics of Quantitative Type Theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 56-65. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209189.
  3. P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 121-135. Springer, 1994. URL: https://doi.org/10.1007/BFB0022251.
  4. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. Linear Haskell: practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang., 2(POPL):5:1-5:29, 2018. URL: https://doi.org/10.1145/3158093.
  5. Flavien Breuvart and Michele Pagani. Modelling coeffects in the relational semantics of linear logic. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, pages 567-581, 2015. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.567.
  6. Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coeffect calculus. In Zhong Shao, editor, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8410 of Lecture Notes in Computer Science, pages 351-370. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54833-8_19.
  7. Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. A graded dependent type system with a usage-aware semantics. Proc. ACM Program. Lang., 5(POPL):1-32, 2021. URL: https://doi.org/10.1145/3434331.
  8. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The Structure of Exponentials: Uncovering the Dynamics of Linear Logic Proofs. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, Brno, Czech Republic, August 24-27, 1993, Proceedings, volume 713 of Lecture Notes in Computer Science, pages 159-171. Springer, 1993. URL: https://doi.org/10.1007/BFB0022564.
  9. Loris D'Antoni, Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas Haeberlen, and Benjamin C. Pierce. Sensitivity analysis using type-based constraints. In Proceedings of the 1st Annual Workshop on Functional Programming Concepts in Domain-Specific Languages, FPCDSL@ICFP 2013, Boston, Massachusetts, USA, September 22, 2013, pages 43-50, 2013. URL: https://doi.org/10.1145/2505351.2505353.
  10. Soichiro Fujii, Shin-ya Katsumata, and Paul-André Melliès. Towards a Formal Theory of Graded Monads. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 513-530. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_30.
  11. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 357-370, 2013. URL: https://doi.org/10.1145/2429069.2429113.
  12. Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, and Tarmo Uustalu. Combining effects and coeffects via grading. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 476-489, 2016. URL: https://doi.org/10.1145/2951913.2951939.
  13. Dan R. Ghica and Alex I. Smith. Bounded linear types in a resource semiring. In Zhong Shao, editor, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8410 of Lecture Notes in Computer Science, pages 331-350. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54833-8_18.
  14. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  15. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci., 97(1):1-66, 1992. URL: https://doi.org/10.1016/0304-3975(92)90386-T.
  16. Peter Hanukaev and Harley Eades III. Combining dependency, grades, and adjoint logic. In Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe 2023, pages 58-70, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3609027.3609408.
  17. Dana Harrington. Uniqueness logic. Theor. Comput. Sci., 354(1):24-41, 2006. URL: https://doi.org/10.1016/j.tcs.2005.11.006.
  18. Jack Hughes, Danielle Marshall, James Wood, and Dominic Orchard. Linear Exponentials as Graded Modal Types. In 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Rome (virtual), Italy, June 2021. URL: https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271465.
  19. Jack Hughes and Dominic Orchard. Program synthesis from graded types. In Stephanie Weirich, editor, Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14576 of Lecture Notes in Computer Science, pages 83-112. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57262-3_4.
  20. Harley Eades III and Dominic Orchard. Grading adjoint logic. CoRR, abs/2006.08854, 2020. URL: https://arxiv.org/abs/2006.08854.
  21. Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka. Adjoint Natural Deduction. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, volume 299 of LIPIcs, pages 15:1-15:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.FSCD.2024.15.
  22. Max I. Kanovich, Stepan L. Kuznetsov, Vivek Nigam, and Andre Scedrov. Soft subexponentials and multiplexing. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pages 500-517. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_29.
  23. Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 633-646. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535846.
  24. Shin-ya Katsumata. A double category theoretic analysis of graded linear exponential comonads. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10803 of Lecture Notes in Computer Science, pages 110-127. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_6.
  25. Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154-170, 1958. Google Scholar
  26. Danielle Marshall and Dominic Orchard. Functional Ownership through Fractional Uniqueness. Proc. ACM Program. Lang., 8(OOPSLA1):1040-1070, 2024. URL: https://doi.org/10.1145/3649848.
  27. Danielle Marshall, Michael Vollmer, and Dominic Orchard. Linearity and Uniqueness: An Entente Cordiale. In Ilya Sergey, editor, Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13240 of Lecture Notes in Computer Science, pages 346-375. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_13.
  28. Conor McBride. I Got Plenty o' Nuttin'. In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella, editors, A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pages 207-233. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_12.
  29. Paul-André Melliès. Categorical semantics of linear logic. In Pierre-Louis Curien, Hugo Herbelin, Jean-Louis Krivine, and Paul-André Melliès, editors, Interactive Models of Computation and Program Behaviour. Panoramas et Synthèses 27, Société Mathématique de France, 2009. Google Scholar
  30. Benjamin Moon, Harley Eades III, and Dominic Orchard. Graded modal dependent type theory. In Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, pages 462-490, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_17.
  31. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang., 3(ICFP):110:1-110:30, 2019. URL: https://doi.org/10.1145/3341714.
  32. Dominic A. Orchard, Tomas Petricek, and Alan Mycroft. The semantic marriage of monads and effects. CoRR, abs/1401.5391, 2014. URL: https://arxiv.org/abs/1401.5391.
  33. Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. Coeffects: Unified static analysis of context-dependence. In Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, pages 385-397, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_35.
  34. Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. Coeffects: a calculus of context-dependent computation. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, pages 123-135, 2014. URL: https://doi.org/10.1145/2628136.2628160.
  35. Frank Pfenning and Dennis Griffith. Polarized substructural session types. In Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9034 of Lecture Notes in Computer Science, pages 3-22. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_1.
  36. Elaine Pimentel, Carlos Olarte, and Vivek Nigam. Process-as-formula interpretation: A substructural multimodal view (invited talk). In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 3:1-3:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.3.
  37. Klaas Pruiksma, William Chargin, Frank Pfenning, and Jason Reed. Adjoint logic. Unpublished Draft: http://www.cs.cmu.edu/~fp/papers/adjoint18b.pdf, 2018.
  38. Klaas Pruiksma and Frank Pfenning. A message-passing interpretation of adjoint logic. Journal of Logical and Algebraic Methods in Programming, page 100637, 2020. Google Scholar
  39. Greg Restall. An introduction to substructural logics. Routledge, 2002. Google Scholar
  40. Victoria Vollmer, Danielle Marshall, Harley Eades III, and Dominic Orchard. A Mixed Linear and Graded Logic: Proofs, Terms, and Models. CoRR, abs/2401.17199, 2024. URL: https://doi.org/10.48550/arXiv.2401.17199.
  41. Jan von Plato. A proof of Gentzen’s Hauptsatz without multicut. Arch. Math. Log., 40(1):9-18, 2001. URL: https://doi.org/10.1007/S001530050170.
  42. Philip Wadler. Linear types can change the world! In Manfred Broy and Cliff B. Jones, editors, Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990, page 561. North-Holland, 1990. Google Scholar
  43. David Walker. Substructural type systems. Advanced topics in types and programming languages, pages 3-44, 2005. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact