Document Open Access Logo

The Logic of Intersection Subtyping

Author Olivier Laurent

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.62.pdf
  • Filesize: 0.98 MB
  • 26 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Linear logic
  • Theory of computation → Lambda calculus
Keywords
  • Intersection types
  • subtyping
  • polymorphic subtyping
  • Lambek calculus
  • linear logic
  • cut elimination

Metrics

Abstract

The subtyping relation of programming languages can be analysed as an entailment relation by means of proof theory. We are interested in two main families of systems: intersection types and polymorphic subtyping. They share the fact that implication has some distributivity property: over intersection in the first case and over universal quantification in the second one.
We introduce a restriction of the second-order (full) Lambek calculus which is stable under cut-elimination and conservatively extends these two subtyping relations. This new system IS is an intuitionistic non-commutative linear sequent calculus which provides a natural logical setting for the study of subtyping relations.
We recover sequent calculi from the literature (as well as new variants) as restrictions of IS (thanks to the proof-theoretical analysis of the system: admissible rules, invertibility, focusing, etc.), so that IS appears as a unifying logic for subtyping. We also develop translations relating IS with relevant logic, the (unconstrained) Lambek calculus or cyclic linear logic.

Cite As Get BibTex

Olivier Laurent. The Logic of Intersection Subtyping. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 62:1-62:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.62

Author Details

Olivier Laurent
  • CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP, UMR 5668, Lyon, France

Acknowledgements

Thanks to A. Dudenhefner for many fruitful discussions about intersection types, and to the anonymous reviewers for their suggestions for improving the presentation.

Supplementary Materials

References

  1. Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Intersection types and lambda models. Theoretical Computer Science, 355(2):108-126, April 2006. URL: https://doi.org/10.1016/j.tcs.2006.01.004.
  2. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992. URL: https://doi.org/10.1093/logcom/2.3.297.
  3. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48:931-940, 1983. URL: https://doi.org/10.2307/2273659.
  4. Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139032636.
  5. Jan Bessai, Tzu-Chun Chen, Andrej Dudenhefner, Boris Düdder, Ugo de Liguoro, and Jakob Rehof. Mixin composition synthesis based on intersection types. Logical Methods in Computer Science, 14:37, February 2018. URL: https://doi.org/10.23638/LMCS-14(1:18)2018.
  6. Jan Bessai, Jakob Rehof, and Boris Düdder. Fast verified BCD subtyping. In Tiziana Margaria, Susanne Graf, and Kim G. Larsen, editors, Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday, volume 11200 of Lecture Notes in Computer Science, pages 356-371. Springer, June 2019. URL: https://doi.org/10.1007/978-3-030-22348-9_21.
  7. Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The essence of nested composition. In Todd Millstein, editor, 32nd European Conference on Object-Oriented Programming (ECOOP), volume 109 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:33. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2018.22.
  8. Viviana Bono and Jerzy Tiuryn. Products and polymorphic subtypes. Fundamenta Informaticae, 51(1-2):13-41, 2002. URL: https://doi.org/10.3233/FUN-2002-511-203.
  9. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. A new deconstructive logic: linear logic. Journal of Symbolic Logic, 62(3):755-807, September 1997. URL: https://doi.org/10.2307/2275572.
  10. Boris Düdder, Moritz Martens, Jakob Rehof, and Pawel Urzyczyn. Bounded combinatory logic. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 243-258. European Association for Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.243.
  11. Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Number 151 in Studies in Logic and the Foundations of Mathematics. Elsevier, April 2007. URL: https://doi.org/10.1016/S0049-237X(13)70001-6.
  12. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  13. Jean-Yves Girard. Light linear logic. Information and Computation, 143(2):175-204, June 1998. URL: https://doi.org/10.1006/inco.1998.2700.
  14. François Lamarche and Christian Retoré. Proof nets for the Lambek calculus - an overview. In Michele Abrusci and Claudia Casadio, editors, Roma workshop: Proofs and Linguistic Categories, pages 241-262, Bologna, April 1996. CLUEB. URL: https://www.lirmm.fr/~retore/ARTICLES/LaReRoma96.pdf.
  15. Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154-170, March 1958. URL: https://doi.org/10.1080/00029890.1958.11989160.
  16. Olivier Laurent. IS Logic. Software, (visited on 2026-07-01). URL: https://github.com/olaure01/islogic/tree/LICS2026
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26957
  17. Olivier Laurent. A proof of the focusing property of linear logic. Unpublished note, 2004, revised 2017. URL: https://perso.ens-lyon.fr/olivier.laurent/llfoc2.pdf.
  18. Olivier Laurent. A syntactic introduction to intersection types. Unpublished note, April 2012. URL: http://perso.ens-lyon.fr/olivier.laurent/tutinter.pdf.
  19. Olivier Laurent. Intersection subtyping with constructors. In Michele Pagani and Sandra Alves, editors, Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems (DCM 2018 and ITRS 2018), volume 293 of Electronic Proceedings in Theoretical Computer Science, pages 73-84. Open Publishing Association, April 2019. URL: https://doi.org/10.4204/EPTCS.293.6.
  20. Olivier Laurent. An anti-locally-nameless approach to formalizing quantifiers. In Catalin Hritcu and Andrei Popescu, editors, CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 300-312. ACM, January 2021. URL: https://doi.org/10.1145/3437992.3439926.
  21. Olivier Laurent. Yalla: Yet another deep embedding of linear logic in Rocq. Journal of Automated Reasoning, 70(9), June 2026. URL: https://doi.org/10.1007/s10817-026-09755-y.
  22. Olivier Laurent and Jui-Hsuan Wu. Non-wellfounded derivations for intersection subtyping with fixpoints. In Frank Pfenning, editor, 11th International Conference on Formal Structures for Computation and Deduction, volume 378 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. URL: https://doi.org/10.4230/LIPIcs.FSCD.2026.22.
  23. Giuseppe Longo, Kathleen Milsted, and Sergei Soloviev. Coherence and transitivity of subtyping as entailment. Journal of Logic and Computation, 10(4):493-526, 2000. URL: https://doi.org/10.1093/LOGCOM/10.4.493.
  24. John C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76(2-3):211-249, 1988. URL: https://doi.org/10.1016/0890-5401(88)90009-0.
  25. David Park. The Y-combinator in Scott’s lambda-calculus models. Technical Report 13, University of Warwick, Department of Computer Science, June 1976. URL: https://wrap.warwick.ac.uk/46310/.
  26. Benjamin C. Pierce. A decision procedure for the subtype relation on intersection types with bounded variables. Technical Report CMU-CS-89-169, School of Computer Science, Carnegie Mellon University, August 1989. URL: https://doi.org/10.1184/R1/6587339.v1.
  27. Richard Routley and Robert K. Meyer. The semantics of entailment - III. Journal of Philosophical Logic, 1:192-208, May 1972. URL: https://doi.org/10.1007/BF00650498.
  28. Yury Savateev. Lambek grammars with one division are decidable in polynomial time. In Edward A. Hirsch, Alexander A. Razborov, Alexei Semenov, and Anatol Slissenko, editors, Computer Science - Theory and Applications, Third International Computer Science Symposium (CSR), pages 273-282. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-79709-8_28.
  29. Harold Schellinx. Some syntactical observations on linear logic. Journal of Logic and Computation, 1(4):537-559, 1991. URL: https://doi.org/10.1093/logcom/1.4.537.
  30. Jürgen Schulte Mönting. Cut elimination and word problems for varieties of lattices. Algebra Universalis, 12:290-321, December 1981. URL: https://doi.org/10.1007/BF02483891.
  31. Dana Scott. Continuous lattices. In Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97-136. Springer, 1972. URL: https://doi.org/10.1007/BFb0073967.
  32. Jerzy Tiuryn. A sequent calculus for subtyping polymorphic types. Information and Computation, 164(2):345-369, 2001. URL: https://doi.org/10.1006/inco.2000.2941.
  33. Jerzy Tiuryn and Pawel Urzyczyn. The subtyping problem for second-order types in undecidable. Information and Computation, 179(1):1-18, November 2002. URL: https://doi.org/10.1006/inco.2001.2950.
  34. Betti Venneri. Intersection types as logical formulae. Journal of Logic and Computation, 4(2):109-124, April 1994. URL: https://doi.org/10.1093/logcom/4.2.109.
  35. Philip Whitman. Free lattices. Annals of Mathematics, 42(1):325-330, January 1941. URL: https://doi.org/10.2307/1969001.
  36. David N. Yetter. Quantales and (noncommutative) linear logic. Journal of Symbolic Logic, 55(1):41-64, 1990. URL: https://doi.org/10.2307/2274953.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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