2026-07-20T02:01:00Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26367 2026-07-15T06:01:57Z ddc:004 open_access

A Bounded Parallel Intersection Type System Dudenhefner, Andrej Schubert, Aleksy Rehof, Jakob type system lambda-calculus intersection types inhabitation complexity 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrej Dudenhefner and Aleksy Schubert and Jakob Rehof 2026 Is Part Of LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2026.17 urn:nbn:de:0030-drops-263679 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.17 eng https://creativecommons.org/licenses/by/4.0/legalcode