| 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 extensionof 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.
|
|---|