**Abstract:**

We introduce a refinement of the lambda-calculus, where
each argument of a function has an explicit multiplicity, indicating
how many copies of it are available. The management of these
resources is done by means of explicit substitutions (with
multiplicity). We show that the resulting calculus has a natural
functionality theory, in the sense of Curry, in a fragment of Girard's
linear logic. In particular we show a refinement of a result of Coppo
and Dezani, namely that a term is convergent if and only if it has a
non-trivial functional character.

[PostScript, .ps.gz ]