In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones.

We prove that type systems are able to capture exact measures related to dynamic properties of functional programs with control operators, which allow implementing intricate continuations and backtracking. Our type systems give the number of evaluation steps to normal form as well as the size of this normal form without any evaluation being needed.

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.

Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type Ω, the auto-autoapplication and they thus do not ensure any form of normalization/productivity. Moreover, in most infinitary frameworks, it is not difficult to define a type R that can be assigned to every λ-term. However, these observations do not say much about what coinductive (i.e. infinitary) type grammars are able to provide: it is for instance very difficult to know what types (besides R) can be assigned to a given term in this setting. We begin with a discussion on the expressivity of different forms of infinite types. Then, using the resource-awareness of sequential intersection types (system S) and tracking, we prove that infinite types are able to characterize the arity of every λ-terms and that, in the infinitary extension of the relational model, every term has a "meaning" i.e. a non-empty denotation. From the technical point of view, we must deal with the total lack of guarantee of productivity for typable terms: we do so by importing methods inspired by first order model theory.

Starting from an exact correspondence between linear approximations and non-idempotent intersection types, we develop a general framework for building systems of intersection types characterizing normalization properties. We show how this construction, which uses in a fundamental way Melliès and Zeilberger's ``type systems as functors'' viewpoint, allows us to recover equivalent versions of every well known intersection type system (including Coppo and Dezani's original system, as well as its non-idempotent variants independently introduced by Gardner and de Carvalho). We also show how new systems of intersection types may be built almost automatically in this way.

We provide a type-theoretical characterization of weakly-normalizing terms in an infinitary lambda-calculus. We adapt for this purpose the standard quantitative (with non-idempotent intersections) type assignment system of the lambda-calculus to our infinite calculus. Our work provides a positive answer to a semi-open question known as Klop's Problem, namely, finding out if there is a type system characterizing the set of hereditary head-normalizing (HHN) lambda-terms. Tatsuta showed in 2007 that HHN could not be characterized by a finite type system. We prove that an infinitary type system endowed with a validity condition called approximability can achieve it. As it turns out, approximability cannot be expressed when intersection is represented by means of multisets. Multisets are then replaced coinductively by sequences of types indexed by integers, thus defining a type system called System S.