Summary: In the first part of this paper, we define two resource aware typing systems for the \(\lambda\mu\)-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments – based on decreasing measures of type derivations – to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head reduction and the maximal reduction sequences to normal-form.
In the second part of this paper, the \(\lambda\mu\)-calculus is refined to a small-step calculus called \(\lambda\mu\)s, which is inspired by the substitution at a distance paradigm. The \(\lambda\mu\)s-calculus turns out to be compatible with a natural extension of the non-idempotent interpretations of \(\lambda\mu\), i.e., \(\lambda\mu\)s-reduction preserves and decreases typing derivations in an extended appropriate typing system. We thus derive a simple arithmetical characterization of strongly \(\lambda\mu\)s-normalizing terms by means of typing.