This thesis deals with the management of explicit resources in functional languages, stressing on properties of calculi with explicit substitutions refining the lambda-calculus. In the first part, we are concerned with the preservation property of beta-strong normalisation (PSN) for the lambda s-calculus, a language among the eight calculi of the prismoid of resources defined thereafter. In the second part, we study the confluence property for a large set of calculi with explicit substitutions. After having given a generic proof of confluence based on a series of axioms that a calculus must fulfill to verify this property, we focalise on the metaconfluence of lambda j, a calculus where the propagation mechanism of substitutions uses the notion of multiplicity, whereas the traditional way is the structural propagation. In the third part, we define a prismoid of resources which generalise in a parametric way the lambda-calculus in the sense that not only the substitution can be explicit, but also the contraction and the weakening. This gives a set of eight calculi spread over the vertices of the prismoid for which we prove in a uniform way several properties of good behavior as the simulation of beta-reduction, PSN, confluence, and strong normalisation for typed terms. In the last part of the thesis we show different opening up to more practical domains. First, we are concerned with the complexity of a calculus with substitutions. We present research tools and conjecture on maximal bounds for reductions of the lambda x-calculus . Finally, we give a formal specification of the lambda j-calculus within the proof assistant Coq.
