Complexity theory helps us predict and control resources, usually time and space, consumed by programs. Static analysis on specific syntactic criterion allows us to categorize some programs. A common approach is to observe the program’s data’s behavior. For instance, the detection of non-size-increasing programs is based on a simple principle : counting memory allocation and deallocation, particularly in loops. This way, we can detect programs which compute within a constant amount of space. This method can easily be expressed as property on control flow graphs. Because analyses on data’s behaviour are syntactic, they can be done at compile time. Because they are only static, those analyses are not always computable or easily computable and approximations are needed. “Size-Change Principle” from C. S. Lee, N. D. Jones et A. M. Ben-Amram presented a method to predict termination by observing resources evolution and a lot of research came from this theory. Until now, these implicit complexity theories were essentially applied on more or less toy languages. This thesis applies implicit computational complexity methods into “real life” programs by manipulating intermediate representation languages in compilers. This give an accurate idea of the actual expressivity of these analyses and show that implicit computational complexity and compilers communities can fuel each other fruitfully. As we show in this thesis, the methods developed are quite generals and open the way to several new applications. / La théorie de la complexité´e s’intéresse à la gestion des ressources, temps ou espace, consommés par un programmel ors de son exécution. L’analyse statique nous permet de rechercher certains critères syntaxiques afin de catégoriser des familles de programmes. L’une des approches les plus fructueuses dans le domaine consiste à observer le comportement potentiel des données manipulées. Par exemple, la détection de programmes “non size increasing” se base sur le principe très simple de compter le nombre d’allocations et de dé-allocations de mémoire, en particulier au cours de boucles et on arrive ainsi à détecter les programmes calculant en espace constant. Cette méthode s’exprime très bien comme propriété sur les graphes de flot de contrôle. Comme les méthodes de complexité implicite fonctionnent à l’aide de critères purement syntaxiques, ces analyses peuvent être faites au moment de la compilation. Parce qu’elles ne sont ici que statiques, ces analyses ne sont pas toujours calculables ou facilement calculables, des compromis doivent être faits en s’autorisant des approximations. Dans le sillon du “Size-Change Principle” de C. S. Lee, N. D. Jones et A. M. Ben-Amram, beaucoup de recherches reprennent cette méthode de prédiction de terminaison par observation de l’évolution des ressources. Pour le moment, ces méthodes venant des théories de la complexité implicite ont surtout été appliquées sur des langages plus ou moins jouets. Cette thèse tend à porter ces méthodes sur de “vrais” langages de programmation en s’appliquant au niveau des représentations intermédiaires dans des compilateurs largement utilises. Elle fournit à la communauté un outil permettant de traiter une grande quantité d’exemples et d’avoir une idée plus précise de l’expressivité réelle de ces analyses. De plus cette thèse crée un pont entre deux communautés, celle de la complexité implicite et celle de la compilation, montrant ainsi que chacune peut apporter à l’autre.

Il existe de nombreuses approches développées par la communauté Implicit Computational Complexity (ICC) permettant d'analyser les ressources nécessaires à la bonne exécution des algorithmes. Dans cette thèse, nous nous intéressons plus particulièrement au contrôle des ressources à l'aide d'interprétations sémantiques. <br />Après avoir rappelé brièvement la notion de quasi-interprétation ainsi que les différentes propriétés et caractérisations qui en découlent, nous présentons les différentes avancées obtenues dans l'étude de cet outil : nous étudions le problème de la synthèse qui consiste à trouver une quasi-interprétation pour un programme donné, puis, nous abordons la question de la modularité des quasi-interprétations. La modularité permet de diminuer la complexité de la procédure de synthèse et de capturer un plus grand nombre d'algorithmes. Après avoir mentionné différentes extensions des quasi-interprétations à des langages de programmation réactif, bytecode ou d'ordre supérieur, nous introduisons la sup-interprétation. Cette notion généralise la quasi-interprétation et est utilisée dans des critères de contrôle des ressources afin d'étudier la complexité d'un plus grand nombre d'algorithmes dont des algorithmes sur des données infinies ou des algorithmes de type diviser pour régner. Nous combinons cette notion à différents critères de terminaison comme les ordres RPO, les paires de dépendance ou le size-change principle et nous la comparons à la notion de quasi-interprétation. En outre, après avoir caractérisé des petites classes de complexité parallèles, nous donnons quelques heuristiques permettant de synthétiser des sup-interprétations sans la propriété sous-terme, c'est à dire des sup-interprétations qui ne sont pas des quasi-interprétations. Enfin, dans un dernier chapitre, nous adaptons les sup-interprétations à des langages orientés-objet, obtenant ainsi différents critères pour contrôler les ressources d'un programme objet et de ses méthodes.

Il existe de nombreuses approches développées par la communauté Implicit Computational Complexity (ICC) permettant d'analyser les ressources nécessaires à la bonne exécution des algorithmes. Dans cette thèse, nous nous intéressons plus particulièrement au contrôle des ressources à l'aide d'interprétations sémantiques. Après avoir rappelé brièvement la notion de quasi-interprétation ainsi que les différentes propriétés et caractérisations qui en découlent, nous présentons les différentes avancées obtenues dans l'étude de cet outil : nous étudions le problème de la synthèse qui consiste à trouver une quasi-interprétation pour un programme donné, puis, nous abordons la question de la modularité des quasi-interprétations. La modularité permet de diminuer la complexité de la procédure de synthèse et de capturer un plus grand nombre d'algorithmes. Après avoir mentionné différentes extensions des quasi-interprétations à des langages de programmation réactifs, bytecode ou d'ordre supérieur, nous introduisons la sup-interprétation. Cette notion généralise la quasi-interprétation et est utilisée dans des critères de contrôle des ressources afin d'étudier la complexité d'un plus grand nombre d'algorithmes dont des algorithmes sur des données infinies ou des algorithmes de type diviser pour régner. Nous combinons cette notion à différents critères de terminaison comme les ordres RPO, les paires de dépendance ou le size-change principle et nous la comparons à la notion de quasi-interprétation. En outre, après avoir caractérisé des petites classes de complexité parallèles, nous donnons quelques heuristiques permettant de synthétiser des sup-interprétations sans la propriété sous-terme, c'est à dire des sup-interprétations qui ne sont pas des quasi-interprétations. Enfin, dans un dernier chapitre, nous adaptons les sup-interprétations à des langages orientés-objet, obtenant ainsi différents critères pour contrôler les ressources d'un programme objet et de ses méthodes / There are several approaches developed by the Implicit Computational Complexity (ICC) community which try to analyze and control program resources. In this document, we focus our study on the resource control with the help of semantics interpretations. After introducing the notion of quasi-interpretation together with its distinct properties and characterizations, we show the results obtained in the study of such a tool: We study the synthesis problem which consists in finding a quasi-interpretation for a given program and we tackle the issue of quasi-interpretation modularity. Modularity allows to decrease the complexity of the synthesis procedure and to capture more algorithms. We present several extensions of quasi-interpretations to reactive programming, bytecode verification or higher-order programming. Afterwards, we introduce the notion of sup-interpretation. This notion strictly generalizes the one of quasi-interpretation and is used in distinct criteria in order to control the resources of more algorithms, including algorithms over infinite data and algorithms using a divide and conquer strategy. We combine sup-interpretations with distinct termination criteria, such as RPO orderings, dependency pairs or size-change principle, and we compare them to the notion of quasi-interpretation. Using the notion of sup-interpretation, we characterize small parallel complexity classes. We provide some heuristics for the sup-interpretation synthesis: we manage to synthesize sup-interpretations without the subterm property, that is, sup-interpretations which are not quasi-interpretations. Finally, we extend sup-interpretations to object-oriented programs, thus obtaining distinct criteria for resource control of object-oriented programs and their methods

Dans la première partie, on propose un système de type pour le lambda-calcul, dans le style du calcul des séquents, nomme « Soft Type Assignment » (STA) qui est inspiré par la logique linéaire « soft ». STA a la propriété de réduction du sujet et est correct et complète pour les calculs en temps polynomial. Par la suite on propose un déduction naturelle, STA_N. Ce système est simple mais il a le désavantage que les variables dans le sujet peuvent être explicitement renommées. Pour résoudre ce problème, on propose le système STA_M, où les contextes sont des multi-ensembles, donc les règles pour renommer les variables peuvent être interdit. L’inférence de type pour STA_M ne semble pas décidable. On propose un algorithme qui pour chaque lambda-terme rend l’ensemble de contraintes que doivent être satisfait pour que le terme soit type. Pi est correct et complet. Ensuite on étend le lambda-calcul par des constantes booléennes et on propose le système STA_B. La particularité de STA_B est que la règle du conditionnel utilise les contextes de façon additive. Chaque programme de STA_B peut être exécuté, par une machine abstraite, en espace polynomial. De plus le système est aussi complet pour PSPACE. Dans la deuxième partie, on propose une restriction de PCF, nommée SlPCF. Ce langage est équipé avec une sémantique opérationnelle qui mélange l’appelle par nom et l’appelle par valeur et peut être interprèté en mode standard dans les espaces cohérents linéaires. SlPCF est complet pour les fonctions récursives, mais il n’est pas complet et donc il n’est pas fully abstract pour les espaces cohérents linéaires / In the first part, we propose, inspired by Soft Linear Logic, a type assignment system for lambda-calculus in sequent calculus style, named Soft Type Assignment (STA). STA enjoys the subject reduction property. and is correct and complete for polynomial time computations. Then, we propose a natural deduction named STA_N. While simple, STA_N has the disadvantage of allowing the explicit renaming of variables in the subject. To overcome to this problem, we propose another natural deduction system, named STA_M, where contexts are multisets, hence rules renaming variables can be avoided. The type inference for STA_M seems in general undecidable. We propose an algorithm Pi returning, for every lambda-term, a set of constraints that need to be satisfied in order to type the term. Pi is correct and complete. We extend the lambda-calculus by basic boolean constants and we propose the system STA_B. The peculiarity of STA_B is that the conditional rule treats the contexts in an additive way. Every STA_B program can be executed, through an abstract machine, in polynomial space. Moreover, STA_B is also complete for PSPACE. In the second part we propose a restriction of PCF, named SlPCF. The language is naturally equipped with an operational semantics mixing call-by-name and call-by-value parameter passing and it can be interpreted in linear coherence space in a standard way. SlPCF is recursive complete, but it is not complete, and thus not fully abstract, with respect to linear coherence spaces

Les résultats de Colson ou de Moschovakis remettent en question que le modèle récursif primitif puisse calculer une valeur par tous les moyens possibles : il y a toutes les fonctions voulues mais il manque des algorithmes. La thèse de Church exprime donc plutôt ce qui peut être calculé que comment le calcul est fait. Nous utilisons la thèse de Gurevich formalisant l'idée intuitive d'algorithme séquentiel par les Abstract States Machines (ASMs).Nous représentons les programmes impératifs par le langage While de Jones, et une variante LoopC du langage de Meyer et Ritchie permettant de sortir d'une boucle lorsqu'une condition est remplie. Nous dirons qu'un langage caractérise une classe algorithmique si les modèles de calcul associés peuvent se simuler mutuellement, en utilisant une dilatation temporelle et un nombre borné de variables temporaires. Nous prouvons que les ASMs peuvent simuler While et LoopC, que si l'espace est primitif récursif alors LoopC est en temps récursif primitif, et que sa restriction LoopC_stat où les bornes des boucles ne peuvent être mises à jour est en temps polynomial. Réciproquement, une étape d'ASM peut être traduite par un programme sans boucle, qu'on peut répéter suffisamment en l'insérant dans un programme qui est dans While si la complexité est quelconque, dans LoopC si elle est récursif primitif, et dans LoopC_stat si elle est polynomiale.Ainsi While caractérise les algorithmes séquentiels en temps quelconque, LoopC ceux en temps et espace récursifs primitifs, et LoopC_stat ceux en temps polynomial / Colson and Moschovakis results cast doubt on the ability of the primitive recursive model to compute a value by any means possible : the model may be complete for functions but there is a lack of algorithms. So the Church thesis express more what can be computed than how the computation is done. We use Gurevich thesis to formalize the intuitive idea of sequential algorithm by the Abstract States Machines (ASMs).We formalize the imperative programs by Jones' While language, and a variation LoopC of Meyer and Ritchie's language allowing to exit a loop if some condition is fulfilled. We say that a language characterizes an algorithmic class if the associated models of computations can simulate each other using a temporal dilatation and a bounded number of temporary variables. We prove that the ASMs can simulate While and LoopC, that if the space is primitive recursive then LoopC is primitive recursive in time, and that its restriction LoopC_stat where the bounds of the loops cannot be updated is in polynomial time. Reciprocally, one step of an ASM can be translated into a program without loop, which can be repeated enough times if we insert it onto a program in While for a general complexity, in LoopC for a primitive recursive complexity, and in LoopC_stat for a polynomial complexity.So While characterizes the sequential algorithms, LoopC the algorithms in primitive recursive space and time, and LoopC_stat the polynomial time algorithms

La logique linéaire fait désormais partie des outils standards en théorie de la démonstration et, de manière plus générale, dans l'étude de la correspondance de Curry-Howard. Nous présentons ici trois directions importantes d'application de méthodes issues de la logique linéaire : - la théorie de la démonstration de la logique classique et ses aspects calculatoires via notamment la sémantique des jeux ; - la complexité implicite à travers les modèles dénotationnels des logiques linéaires à complexité bornée ; - la théorie de la concurrence et ses fondements logiques grâce aux ingrédients apportés par la logique linéaire différentielle. Les approches linéaires offrent ainsi un cadre commun pour l'étude de différents aspects logiques du calcul.

La complexité implicite (ICC) vise à donner des caractérisations de classes de complexité dans des langages de programmation ou des logiques, sans faire référence à des bornes sur les ressources (temps, espace mémoire). Dans cette thèse, nous étudions l’approche de la logique linéaire à la complexité implicite. L’objectif est de donner des caractérisations de classes de complexité, à travers des variantes du lambda-calcul qui sont typables dans de tels systèmes. En particulier, nous considérons à la fois une perspective monovalente et une perspective polyvalente par rapport à l’ICC. Dans le premier cas, le but est de caractériser une hiérarchie de classes de complexité à travers un lambda-calcul élémentaire typé dans la logique linéaire élémentaire (ELL), où la complexité ne dépend que de l’interface d’un programme, c’est à dire son type. La deuxième approche rend compte à la fois des fonctions calculables en temps polynomial et de la normalisation forte, à travers des termes du lambda-calcul pur qui sont typés dans un système inspiré par la logique linéaire Soft (SLL); en particulier, par rapport à l’approche logique ordinaire, ici nous abandonnons la modalité “!” en faveur de l’emploi des types stratifiés, vus comme un raffinement des types intersection non associatifs, afin d’améliorer la typabilité et, en conséquence, l’expressivité. Enfin, nous explorons l’utilisation des types intersection, privés de certaines de leurs propriétés, vers une direction plus quantitative que l’approche qualitative habituelle, afin d’obtenir une borne sur le calcul de lambda-termes purs, en obtenant en plus une caractérisation de la normalisation forte. / In this thesis we explore the linear logic approach to implicit computational complexity, through the design of type assignment systems based on light linear logic, or heavily inspired by them, with the purpose of giving a characterization of one or more complexity classes, through variants of lambda-calculi which are typable in such systems. In particular, we consider both a monovalent and a polyvalent perspective with respect to ICC. In the first one the aim is to characterize a hierarchy of complexity classes through an elementary lambda-calculus typed in Elementary Linear Logic (ELL), where the complexity depends only on the interface of a term, namely its type. The second approach gives an account of both the functions computable in polynomial time and of strong normalization, through terms of pure lambda-calculus which are typed in a system inspired by Soft Linear Logic (SLL); in particular, with respect to the usual logical take, in the latter we give up the “!” modality in favor of employing stratified types as a refinement of non-associative intersection types, in order to improve typability and, as a consequence, expressivity.Finally we explore the use of intersection types, deprived of some of their usual properties, towards a more quantitative approach rather than the usual qualitative one, namely in order to compute a bound on the computation of pure lambda-terms, obtaining in addition a characterization of strong normalization.

La complexité implicite est la caractérisation de classes de complexité par des restrictions syntaxiques sur des modèles de calcul. Plusieurs sous-systèmes de la logique linéaire caractérisant le temps polynomial ont été définis: ces systèmes sont corrects (les termes normalisent en temps polynomial) et complets (il est possible de simuler une machine de Turing pendant un nombre polynomial d'étapes). Un des buts sur le long terme est de donner statiquement des bornes de complexité. C’est pourquoi nous cherchons les caractérisations du temps polynomial les plus expressives possible. Notre principal outil est la sémantique des contextes: des jetons voyagent à travers le réseau selon certaines règles. Les chemins définis par ces jetons représentent la réduction du réseau. Contrairement aux travaux précédents, nous ne définissons pas directement des sous-systèmes de la logique linéaire. Nous définissons d'abord des relations -> sur les sous-termes des réseaux de preuves tel que: B -> C ssi ”le nombre de copies de B dépend du nombre de copies de C”. L’acyclicité de -> borne le nombre de copies de chaque sous-terme, donc la complexité du terme. Ensuite nous définissons des sous-systèmes de la logique linéaire assurant l’acyclicité de ->. Nous étudions aussi des caractérisations du temps élémentaire et primitif récursif. Dans le but d’adapter nos sous-systèmes de la logique linéaire à des langages plus riches, nous adaptons la sémantique des contextes aux réseaux d’interaction, utilisés comme langage cible pour de petits langage de programmation. Nous utilisons cette sémantique des contexte pour définir une sémantique dénotationnelle sur les réseaux d’interactions. / Implicit computational complexity is the characterization of complexity classes by syntactic restrictions on computation models. Several subsystems of linear logic characterizing polynomial time have been defined : these systems are sound (terms normalize in polynomial time) and complete (it is possible to simulate a Turing machine during a polynomial number of steps). One of the long term goals is to statically prove complexity bounds. This is why we are looking for the most expressive characterizations possible. Our main tool is context semantics : tokens travel across proof-nets (programs of linear logic) according to some rules. The paths defined by these tokens represent the reduction of the proof-net.Contrary to previous works, we do not directly define subsystems of linear logic. We first define relations -> on subterms of proof-nets such that: B -> C means \the number of copies of B depends on the number of copies of C". The acyclicity of -> allows us to bound the number of copies of any subterm, this bounds the complexity of the term. Then, we define subsystems of linear logic guaranteeing the acyclicity of ->. We also study characterizations of elementary time and primitive recursive time. In orderto adapt our linear logic subsystems to richer languages, we adapt the context semantics to interaction nets, used as a target language for small programming languages. We use this context semantics to define a denotational semantics on interaction nets.

On étudie dans cette thèse une structure de semi-anneau dont le produit est basé sur la règle de résolution de la programmation logique. Cet objet mathématique a été initialement introduit dans le but de modéliser la procédure d'élimination des coupures de la logique linéaire, dans le cadre du programme de géométrie de l'interaction. Il fournit un cadre algébrique et abstrait, tout en étant présenté sous une forme syntaxique et concrète, dans lequel mener une étude théorique du calcul. On reviendra dans un premier temps sur l'interprétation interactive de la théorie de la démonstration dans ce semi-anneau, via l'axiomatisation catégorique de l'approche de la géométrie de l'interaction. Cette interprétation établit une traduction des programmes fonctionnels vers une forme très simple de programmes logiques. Dans un deuxième temps, on abordera des problématiques de théorie de la complexité: bien que le problème de la nilpotence dans le semi-anneau étudié soit indécidable en général, on fera apparaître des restrictions qui permettent de caractériser le calcul en espace logarithmique (déterministe et non-déterministe) et en temps polynomial (déterministe). / We study in this thesis a semiring structure with a product based on the resolution rule of logic programming. This mathematical object was introduced initially in the setting of the geometry of interaction program in order to model the cut-elimination procedure of linear logic. It provides us with an algebraic and abstract setting, while being presented in a syntactic and concrete way, in which a theoretical study of computation can be carried on. We will review first the interactive interpretation of proof theory within this semiring via the categorical axiomatization of the geometry of interaction approach. This interpretation establishes a way to translate functional programs into a very simple form of logic programs. Secondly, complexity theory problematics will be considered: while the nilpotency problem in the semiring we study is undecidable in general, it will appear that certain restrictions allow for characterizations of (deterministic and non-deterministic) logarithmic space and (deterministic) polynomial time computation.