Andrej Dudenhefner (Univ. Dortmund), Intersection Type Calculi of Bounded Dimension


In the realm of intersection type calculi exist several approaches to restrict or bound the rule of intersection introduction. The most prominent example are non-idempotent intersection types, where types are treated as a linear resource in order to allow for decidable inhabitation. We present a different restriction of the standard intersection type system based on a notion of dimension. Dimension intuitively measures intersection introduction (opposed to intersection types themselves) as a resource via proof theoretic decorations necessary for typing the term at its type. As a result, we have a non-idempotent and non-linear interpretation of intersection that enjoys EXPSPACE-complete inhabitation, vastly generalizing the rank-2 result. Additionally, the induced dimensional analysis of (untyped) lambda calculus lends itself to inspect dimensionality of e.g. normal forms or terms typable in System F.