Characterizing Strongly Normalizing λGtz-terms via Non-Idempotent Intersection Types

Idempotent and non-idempotent intersection type systems have been used in a series of papers for characterizing strong normalization in natural deduction style. Regarding the sequent calculus, only idempotent type systems have been used so far. Strong normalization in the non-idempotent intersection type system follows without requiring reducibility techniques. Non-idempotent intersection type systems are just based on the decrease of a non-negative integer measure. In this paper, we introduce a non-idempotent intersection system for λGtz-calculus, which is in sequent calculus style, to show that a λGtz-term is typeable if and only if it is strongly normalizing.