Controlling the resource consumption of programs is crucial: besides performance reasons, it has many applications in the field of computer security where e.g. mobile or embedded systems dispose of limited amounts of resources. In this thesis, we develop static criteria to control the resource consumption of higher-order concurrent programs. Our starting point is the framework of Light Logics which has been extensively studied to control the complexity of higher-order functional programs through the proofs-as-programs correspondence. The contribution of this thesis is to extend this framework to higher-order concurrent programs. More generally, this thesis fits in the research field of Implicit Computational Complexity which aims at characterizing complexity classes by logical principles or language restrictions. The criteria that we propose are purely syntactic and are developed gradually to control the computational time of programs in a finer and finer way: first, we show how to guarantee the termination of programs (finite time); then, we show how to guarantee the termination of programs in elementary time and last, we show how to guarantee the termination of programs in polynomial time. We also introduce type systems so that well-typed programs are guaranteed to terminate in bounded time and to return values. Finally, we show that the type systems capture some interesting concurrent programs that iterate functions producing side effects over inductive data structures. In the last part, we study an alternative semantic method to control the resource consumption of higher-order imperative programs. The method is based on Dal Lago and Hofmann's quantitative realizability framework and allows to obtain various complexity bounds in a uniform way. This last part is joint work with Aloïs Brunel.
