Document Open Access Logo

A Bounded Parallel Intersection Type System

Authors Andrej Dudenhefner , Aleksy Schubert , Jakob Rehof

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.17.pdf
  • Filesize: 0.82 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • type system
  • lambda-calculus
  • intersection types
  • inhabitation
  • complexity

Metrics

Abstract

We introduce a new presentation of the intersection type discipline in which typing judgments derive vectors of types rather than single types. The system uses binary relations to control the flow of information between coordinates of these vectors. We refer to this presentation as system R. The maximal length of type vectors assigned to variables serves as a reasonable notion of dimension for system R, which allows for a natural stratification into fragments of bounded dimension.
The present system lies strictly between two known bounded-dimensional systems: the multiset-dimensional system, for which inhabitation is EXPSPACE-complete, and the set-dimensional system, for which inhabitation is undecidable. Our main result is that inhabitation in bounded system R is decidable in 2-EXPTIME, while for each fixed dimension, inhabitation is decidable in EXPTIME. This result is based on a subformula property restricting the inhabitant search space. Unlike in traditional intersection type systems, the proof of the subformula property requires careful treatment of the additional information flow management capabilities.
Finally, we argue that system R and its stratification is a valid presentation of the intersection type discipline. First, by proving the subject reduction property for system R in each bounded dimension, and second, by establishing a correspondence with the classical intersection type system of Barendregt, Coppo, and Dezani-Ciancaglini.

Cite As Get BibTex

Andrej Dudenhefner, Aleksy Schubert, and Jakob Rehof. A Bounded Parallel Intersection Type System. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.17

Author Details

Andrej Dudenhefner
  • TU Dortmund University, Germany
Aleksy Schubert
  • University of Warsaw, Poland
Jakob Rehof
  • TU Dortmund University and Lamarr Institute for ML and AI, Germany

References

  1. H. P. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press, 2013. Google Scholar
  2. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symb. Log., 48(4):931-940, 1983. URL: https://doi.org/10.2307/2273659.
  3. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. The inhabitation problem for non-idempotent intersection types. In TCS 2014, Proceedings of 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science, Rome, Italy, September 1-3, 2014. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44602-7_26.
  4. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL, 25(4):431-464, 2017. URL: https://doi.org/10.1093/JIGPAL/JZX018.
  5. M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional Characters of Solvable Terms. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, pages 45-58, 1981. Google Scholar
  6. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci., 28(7):1169-1203, 2018. URL: https://doi.org/10.1017/S0960129516000396.
  7. Andrej Dudenhefner and Jakob Rehof. Intersection type calculi of bounded dimension. POPL 2017, SIGPLAN Not., 52(1):653-665, January 2017. URL: https://doi.org/10.1145/3093333.3009862.
  8. Andrej Dudenhefner and Jakob Rehof. Typability in bounded dimension. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005127.
  9. Andrej Dudenhefner, Christoph Stahl, Constantin Chaumet, Felix Laarmann, and Jakob Rehof. Finite Combinatory Logic with Predicates. In Delia Kesner, Eduardo Hermo Reyes, and Benno van den Berg, editors, 29th International Conference on Types for Proofs and Programs (TYPES 2023), volume 303 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1-2:22, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2023.2.
  10. Andrej Dudenhefner and Paweł Urzyczyn. Kripke semantics for intersection formulas. ACM Trans. Comput. Log., 22(3):15:1-15:16, 2021. URL: https://doi.org/10.1145/3453481.
  11. Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. Example-directed synthesis: a type-theoretic interpretation. POPL 2026, ACM Sigplan Notices, 51(1):802-815, 2016. URL: https://doi.org/10.1145/2837614.2837629.
  12. J. Roger Hindley. The simple semantics for coppo-dezani-sallé types. In Mariangiola Dezani-Ciancaglini and Ugo Montanari, editors, International Symposium on Programming, 5th Colloquium, Torino, Italy, April 6-8, 1982, Proceedings, volume 137 of Lecture Notes in Computer Science, pages 212-226. Springer, 1982. URL: https://doi.org/10.1007/3-540-11494-7_15.
  13. D. Leivant. Polymorphic Type Inference. In POPL 1983, Proceedings of the 10th ACM Symposium on Principles of Programming Languages, pages 88-98, 1983. URL: https://doi.org/10.1145/567067.567077.
  14. Luigi Liquori and Simona Ronchi Della Rocca. Intersection-types à la church. Inf. Comput., 205(9):1371-1386, 2007. URL: https://doi.org/10.1016/J.IC.2007.03.005.
  15. Elaine Pimentel, Simona Ronchi Della Rocca, and Luca Roversi. Intersection types from a proof-theoretic perspective. Fundam. Informaticae, 121(1-4):253-274, 2012. URL: https://doi.org/10.3233/FI-2012-778.
  16. Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. Program synthesis from polymorphic refinement types. PLDI 2016, ACM SIGPLAN Notices, 51(6):522-538, 2016. URL: https://doi.org/10.1145/2908080.2908093.
  17. Simona Ronchi Della Rocca and Luca Roversi. Intersection logic. In Laurent Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001., volume 2142 of Lecture Notes in Computer Science, pages 414-428. Springer, 2001. URL: https://doi.org/10.1007/3-540-44802-0_29.
  18. Simona Ronchi Della Rocca, Alexis Saurin, Yiorgos Stavrinos, and Anastasia Veneti. Intersection logic in sequent calculus style. In Elaine Pimentel, Betti Venneri, and Joe B. Wells, editors, Proceedings Fifth Workshop on Intersection Types and Related Systems, ITRS 2010, Edinburgh, U.K., 9th July 2010., volume 45 of EPTCS, pages 16-30, 2010. URL: https://doi.org/10.4204/EPTCS.45.2.
  19. P. Urzyczyn. Inhabitation of Low-Rank Intersection Types. In TLCA 2009, Proceedings of Typed Lambda Calculus and Applications, volume 5608 of LNCS, pages 356-370. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02273-9_26.
  20. Steffen van Bakel. Complete restrictions of the intersection type discipline. Theoretical Computer Science, 102(1):135-163, 1992. URL: https://doi.org/10.1016/0304-3975(92)90297-S.
  21. Steffen van Bakel. Cut-elimination in the strict intersection type assignment system is strongly normalizing. Notre Dame J. Formal Log., 45(1):35-63, 2004. URL: https://doi.org/10.1305/NDJFL/1094155278.
  22. Steffen van Bakel. Strict intersection types for the lambda calculus. ACM Comput. Surv., 43(3):20:1-20:49, 2011. URL: https://doi.org/10.1145/1922649.1922657.
  23. J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn A. Turbak. A calculus with polymorphic and polyvariant flow types. J. Funct. Program., 12(3):183-227, 2002. URL: https://doi.org/10.1017/S0956796801004245.
  24. Joe B. Wells and Christian Haack. Branching types. In Daniel Le Métayer, editor, Programming Languages and Systems, 11th European Symposium on Programming, ESOP 2002, held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings, volume 2305 of Lecture Notes in Computer Science, pages 115-132. Springer, 2002. URL: https://doi.org/10.1007/3-540-45927-8_9.
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