| Popis: |
Contrôler la consommation en ressources des programmes informatiques est d'importance capitale, non seulement pour des raisons de performance, mais aussi pour des questions de sécurité quand par exemple certains systèmes mobiles ou embarqués disposent de quantités limitées de ressources. Dans cette thèse, nous développons des critères statiques pour contrôler la consommation en ressources de programmes concurrents d'ordre supérieur. Nous prenons comme point de départ le cadre des Logiques Light qui a été étudié afin de contrôler la complexité de programmes fonctionnels d'ordre supérieur au moyen de la correspondance preuves-programmes. La contribution de cette thèse est d'étendre ce cadre aux programmes concurrents d'ordre supérieur. Plus généralement, cette thèse s'inscrit dans le domaine de la complexité implicite qui cherche à caractériser des classes de complexité par des principes logiques ou des restrictions de langage. Les critères que nous proposons sont purement syntaxiques et sont développés graduellement afin de contrôler le temps de calcul des programmes de plus en plus finement: dans un premier temps nous montrons comment garantir la terminaison des programmes (temps fini), puis nous montrons comment garantir la terminaison des programmes en temps élémentaire, et enfin nous montrons comment garantir la terminaison des programmes en temps polynomial. Nous introduisons également des systèmes de types tels que les programmes bien typés terminent en temps borné et retournent des valeurs. Enfin, nous montrons que ces systèmes de types capturent des programmes concurrents intéressants qui itèrent des fonctions produisant des effets de bord sur des structures de données inductives. Dans la dernière partie, nous étudions une méthode sémantique alternative afin de contrôler la consommation en ressources de programmes impératifs d'ordre supérieur. Cette méthode est basée sur la réalisabilité quantitative de Dal Lago et Hofmann et permet d'obtenir plusieurs bornes de complexité de manière uniforme. Cette dernière partie est un travail en collaboration avec Aloïs Brunel. |
