**Abstract:**

The lambda-calculus with resources is a non-deterministic refinement
of the lazy lambda-calculus which provides explicit means to control
the number of times an argument can be used, and introduces the
possibility of raising deadlocks during evaluation. It arose in
connection with Milner's encoding of lazy lambda-calculus into the
pi-calculus and proved to be the correct extension to study the
semantics induced by the pi-calculus over pure lambda-terms. In this
paper, we study a functionality theory in the style of Coppo et al.'s
intersection type system for the calculus of resources extended with
convergence testing. The interpretation of terms in this typing system
gives rise to a fully abstract semantics of the calculus. This is
shown following the definability approach. We also prove that this
semantics is not fully abstract for the calculus without convergence
testing.