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

### Résumé

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.