**Abstract:**

We present the lambda calculus with resources, and two variants of it:
a deterministic restriction, the lambda calculus with multiplicities,
and an extension with a convergence testing operator. These calculi
provide control on the substitution process - deadlocks may arise if
not enough resources are available to carry out all the substitutions
needed to pursue a computation. The design of these calculi was
motivated by Milner's encoding of the lambda calculus in the pi
calculus. As Boudol and Laneve have shown elsewhere, the discriminating
power of the lambda calculus with multiplicities (given by the
contextual observational equivalence) over lambda terms coincides
with that induced by Milner's encoding, and coincides also with that
provided by the lazy algebraic semantics (Levy-Longo trees).
The main contribution of this paper is model-theoretic. We define
and solve an appropriate domain equation, and show that the model
thus obtained is fully abstract for the calculus with convergence testing.
The techniques used are in the line of those used by Abramsky for
the lazy lambda calculus, the main departure being that the
resource-consciousness of our calculi leads us to introduce a
non-idempotent form of intersection types.